let R be non empty interval RelStr ; :: thesis: R is Heyting
thus R is LATTICE ; :: according to WAYBEL_1:def 19 :: thesis: for b1 being Element of the carrier of R holds b1 "/\" is lower_adjoint
let x be Element of R; :: thesis:
set f = x "/\" ;
x "/\" is sups-preserving
proof
let X be Subset of R; :: according to WAYBEL_0:def 33 :: thesis:
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
let b be Element of R; :: thesis: ( b is_>=_than (x "/\") .: X implies (x "/\") . (sup X) <<= b1 )
assume A2: b is_>=_than (x "/\") .: X ; :: thesis: (x "/\") . (sup X) <<= b1
per cases ( x is_>=_than X or not x is_>=_than X ) ;
suppose A3: x is_>=_than X ; :: thesis: (x "/\") . (sup X) <<= b1
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;
then x "/\" a = a by YELLOW_0:25;
then A5: a = (x "/\") . a by WAYBEL_1:def 18;
(x "/\") . a in (x "/\") .: X by ;
hence a <<= b by A2, A5; :: thesis: verum
end;
then A6: b >>= sup X by YELLOW_0:32;
x >>= sup X by ;
then x "/\" (sup X) = sup X by YELLOW_0:25;
hence (x "/\") . (sup X) <<= b by ; :: thesis: verum
end;
suppose not x is_>=_than X ; :: thesis: (x "/\") . (sup X) <<= b1
then consider a being Element of R such that
A7: a in X and
A8: not x >>= a ;
A9: x <<= a by ;
a <<= sup X by ;
then x <<= sup X by ;
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 ;
x = x "/\" a by
.= (x "/\") . a by WAYBEL_1:def 18 ;
hence (x "/\") . (sup X) <<= b by A2, A10, A11; :: 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 ;
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 ;
hence a <<= (x "/\") . (sup X) by ; :: thesis: verum
end;
hence "\/" (((x "/\") .: X),R) = (x "/\") . ("\/" (X,R)) by ; :: thesis: verum
end;
hence x "/\" is lower_adjoint by WAYBEL_1:17; :: thesis: verum