let R be non empty interval RelStr ; R is Heyting
thus
R is LATTICE
; WAYBEL_1:def 19 for b1 being Element of the carrier of R holds b1 "/\" is lower_adjoint
let x be Element of R; x "/\" is lower_adjoint
set f = x "/\" ;
x "/\" is sups-preserving
proof
let X be
Subset of
R;
WAYBEL_0:def 33 x "/\" preserves_sup_of X
assume
ex_sup_of X,
R
;
WAYBEL_0:def 31 ( ex_sup_of (x "/\") .: X,R & "\/" (((x "/\") .: X),R) = (x "/\") . ("\/" (X,R)) )
thus
ex_sup_of (x "/\") .: X,
R
by Th8;
"\/" (((x "/\") .: X),R) = (x "/\") . ("\/" (X,R))
(x "/\") . (sup X) is_>=_than (x "/\") .: X
hence
"\/" (
((x "/\") .: X),
R)
= (x "/\") . ("\/" (X,R))
by A1, YELLOW_0:30;
verum
end;
hence
x "/\" is lower_adjoint
by WAYBEL_1:17; verum