let R be non empty interval RelStr ; :: thesis: R is Heyting
thus R is LATTICE ; :: according to WAYBEL_1:def 19 :: thesis: for b₁ being Element of the carrier of R holds b₁ "/\" is lower_adjoint
let x be Element of R; :: thesis: x "/\" is lower_adjoint
set f = x "/\" ;
x "/\" is sups-preserving

proof

let X be Subset of R; :: according to WAYBEL_0:def 33 :: thesis: x "/\" preserves_sup_of X
assume ex_sup_of X,R ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (x "/\" ) .: X,R & "\/" ((x "/\" ) .: X),R = (x "/\" ) . ("\/" X,R) )

A1: now

let b be Element of R; :: thesis: ( b is_>=_than (x "/\" ) .: X implies (x "/\" ) . (sup X) <<= b₁ )
assume A2: b is_>=_than (x "/\" ) .: X ; :: thesis: (x "/\" ) . (sup X) <<= b₁

per cases ( x is_>=_than X or not x is_>=_than X ) ;

suppose A3: x is_>=_than X ; :: thesis: (x "/\" ) . (sup X) <<= b₁

b is_>=_than X

proof

let a be Element of R; :: according to LATTICE3:def 9 :: thesis: ( not a in X or a <<= b )
assume A4: a in X ; :: thesis: a <<= b
then x >>= a by A3, LATTICE3:def 9;
then x "/\" a = a by YELLOW_0:25;
then A5: a = (x "/\" ) . a by WAYBEL_1:def 18;
(x "/\" ) . a in (x "/\" ) .: X by A4, FUNCT_2:43;
hence a <<= b by A2, A5, LATTICE3:def 9; :: thesis: verum

end;

then A6: b >>= sup X by YELLOW_0:32;
x >>= sup X by A3, YELLOW_0:32;
then x "/\" (sup X) = sup X by YELLOW_0:25;
hence (x "/\" ) . (sup X) <<= b by A6, WAYBEL_1:def 18; :: thesis: verum

end;

suppose not x is_>=_than X ; :: thesis: (x "/\" ) . (sup X) <<= b₁

then consider a being Element of R such that
A7: a in X and
A8: not x >>= a by LATTICE3:def 9;
A9: x <<= a by A8, WAYBEL_0:def 29;
a <<= sup X by A7, YELLOW_2:24;
then x <<= sup X by A9, ORDERS_2:26;
then x = x "/\" (sup X) by YELLOW_0:25;
then A10: x = (x "/\" ) . (sup X) by WAYBEL_1:def 18;
A11: (x "/\" ) . a in (x "/\" ) .: X by A7, FUNCT_2:43;
x = x "/\" a by A9, YELLOW_0:25
.= (x "/\" ) . a by WAYBEL_1:def 18 ;
hence (x "/\" ) . (sup X) <<= b by A2, A10, A11, LATTICE3:def 9; :: thesis: verum

end;

end;

end;

thus ex_sup_of (x "/\" ) .: X,R by Th8; :: thesis: "\/" ((x "/\" ) .: X),R = (x "/\" ) . ("\/" X,R)
(x "/\" ) . (sup X) is_>=_than (x "/\" ) .: X

proof

let a be Element of R; :: according to LATTICE3:def 9 :: thesis: ( not a in (x "/\" ) .: X or a <<= (x "/\" ) . (sup X) )
A12: ( (x "/\" ) . (sup X) = x "/\" (sup X) & x <<= x ) by WAYBEL_1:def 18, YELLOW_0:def 1;
assume a in (x "/\" ) .: X ; :: thesis: a <<= (x "/\" ) . (sup X)
then consider y being set such that
A13: y in the carrier of R and
A14: ( y in X & a = (x "/\" ) . y ) by FUNCT_2:115;
reconsider y = y as Element of R by A13;
( y <<= sup X & a = x "/\" y ) by A14, WAYBEL_1:def 18, YELLOW_2:24;
hence a <<= (x "/\" ) . (sup X) by A12, YELLOW_3:2; :: thesis: verum

end;

hence "\/" ((x "/\" ) .: X),R = (x "/\" ) . ("\/" X,R) by A1, YELLOW_0:30; :: thesis: verum

end;

hence x "/\" is lower_adjoint by WAYBEL_1:18; :: thesis: verum