let R be non empty interval RelStr ; :: thesis: R is Heyting

thus R is LATTICE ; :: according to WAYBEL_1:def 19 :: thesis: for b_{1} being Element of the carrier of R holds b_{1} "/\" is lower_adjoint

let x be Element of R; :: thesis: x "/\" is lower_adjoint

set f = x "/\" ;

x "/\" is sups-preserving

thus R is LATTICE ; :: according to WAYBEL_1:def 19 :: thesis: for b

let x be Element of R; :: thesis: x "/\" is lower_adjoint

set f = x "/\" ;

x "/\" is sups-preserving

proof

hence
x "/\" is lower_adjoint
by WAYBEL_1:17; :: thesis: verum
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)) )

(x "/\") . (sup X) is_>=_than (x "/\") .: X

end;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 :: thesis: for b being Element of R st b is_>=_than (x "/\") .: X holds

(x "/\") . (sup X) <<= b

thus
ex_sup_of (x "/\") .: X,R
by Th8; :: thesis: "\/" (((x "/\") .: X),R) = (x "/\") . ("\/" (X,R))(x "/\") . (sup X) <<= b

let b be Element of R; :: thesis: ( b is_>=_than (x "/\") .: X implies (x "/\") . (sup X) <<= b_{1} )

assume A2: b is_>=_than (x "/\") .: X ; :: thesis: (x "/\") . (sup X) <<= b_{1}

end;assume A2: b is_>=_than (x "/\") .: X ; :: thesis: (x "/\") . (sup X) <<= b

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

end;

suppose A3:
x is_>=_than X
; :: thesis: (x "/\") . (sup X) <<= b_{1}

b is_>=_than X

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;proof

then A6:
b >>= sup X
by YELLOW_0:32;
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;

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:35;

hence a <<= b by A2, A5; :: thesis: verum

end;assume A4: a in X ; :: thesis: a <<= b

then x >>= a by A3;

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:35;

hence a <<= b by A2, A5; :: thesis: verum

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

suppose
not x is_>=_than X
; :: thesis: (x "/\") . (sup X) <<= b_{1}

then consider a being Element of R such that

A7: a in X and

A8: not x >>= a ;

A9: x <<= a by A8, WAYBEL_0:def 29;

a <<= sup X by A7, YELLOW_2:22;

then x <<= sup X by A9, ORDERS_2:3;

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:35;

x = x "/\" a by A9, YELLOW_0:25

.= (x "/\") . a by WAYBEL_1:def 18 ;

hence (x "/\") . (sup X) <<= b by A2, A10, A11; :: thesis: verum

end;A7: a in X and

A8: not x >>= a ;

A9: x <<= a by A8, WAYBEL_0:def 29;

a <<= sup X by A7, YELLOW_2:22;

then x <<= sup X by A9, ORDERS_2:3;

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:35;

x = x "/\" a by A9, YELLOW_0:25

.= (x "/\") . a by WAYBEL_1:def 18 ;

hence (x "/\") . (sup X) <<= b by A2, A10, A11; :: thesis: verum

(x "/\") . (sup X) is_>=_than (x "/\") .: X

proof

hence
"\/" (((x "/\") .: X),R) = (x "/\") . ("\/" (X,R))
by A1, YELLOW_0:30; :: thesis: verum
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 object such that

A13: y in the carrier of R and

A14: ( y in X & a = (x "/\") . y ) by FUNCT_2:64;

reconsider y = y as Element of R by A13;

( y <<= sup X & a = x "/\" y ) by A14, WAYBEL_1:def 18, YELLOW_2:22;

hence a <<= (x "/\") . (sup X) by A12, YELLOW_3:2; :: thesis: verum

end;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 object such that

A13: y in the carrier of R and

A14: ( y in X & a = (x "/\") . y ) by FUNCT_2:64;

reconsider y = y as Element of R by A13;

( y <<= sup X & a = x "/\" y ) by A14, WAYBEL_1:def 18, YELLOW_2:22;

hence a <<= (x "/\") . (sup X) by A12, YELLOW_3:2; :: thesis: verum