let R be non empty interval RelStr ; :: thesis:
thus R is LATTICE ; :: according to WAYBEL_1:def 19 :: thesis:
let x be Element of R; :: thesis:
set f = x "/\" ;
x "/\" is sups-preserving

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:

A1: now :: thesis:

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

suppose A3: x is_>=_than X ; :: thesis:

let a be Element of R; :: according to LATTICE3:def 9 :: thesis:
assume A4: a in X ; :: thesis:
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:

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:

end;

suppose not x is_>=_than X ; :: thesis:

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:

end;

end;

end;

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

let a be Element of R; :: according to LATTICE3:def 9 :: thesis:
A12: ( (x "/\") . (sup X) = x "/\" (sup X) & x <<= x ) by WAYBEL_1:def 18, YELLOW_0:def 1;
assume a in (x "/\") .: X ; :: thesis:
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:

end;

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

end;

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