let L be non empty RelStr ; :: thesis: ( ( for A being Subset of L holds ex_sup_of A,L ) implies for X being set holds
( ex_sup_of X,L & "\/" X,L = "\/" (X /\ the carrier of L),L ) )
assume A1: for A being Subset of L holds ex_sup_of A,L ; :: thesis: for X being set holds
( ex_sup_of X,L & "\/" X,L = "\/" (X /\ the carrier of L),L )
let X be set ; :: thesis: ( ex_sup_of X,L & "\/" X,L = "\/" (X /\ the carrier of L),L )
set Y = X /\ the carrier of L;
set a = "\/" (X /\ the carrier of L),L;
reconsider Y = X /\ the carrier of L as Subset of L by XBOOLE_1:17;
A2: ex_sup_of Y,L by A1;
A3: X is_<=_than "\/" (X /\ the carrier of L),L

proof

let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in X or x <= "\/" (X /\ the carrier of L),L )
assume x in X ; :: thesis: x <= "\/" (X /\ the carrier of L),L
then A4: x in Y by XBOOLE_0:def 4;
Y is_<=_than "\/" (X /\ the carrier of L),L by A2, YELLOW_0:def 9;
hence x <= "\/" (X /\ the carrier of L),L by A4, LATTICE3:def 9; :: thesis: verum

end;

A5: for b being Element of L st X is_<=_than b holds
"\/" (X /\ the carrier of L),L <= b

proof

let b be Element of L; :: thesis: ( X is_<=_than b implies "\/" (X /\ the carrier of L),L <= b )
A6: Y c= X by XBOOLE_1:17;
assume X is_<=_than b ; :: thesis: "\/" (X /\ the carrier of L),L <= b
then Y is_<=_than b by A6, YELLOW_0:9;
hence "\/" (X /\ the carrier of L),L <= b by A2, YELLOW_0:def 9; :: thesis: verum

end;

ex_sup_of X,L by A2, YELLOW_0:50;
hence ( ex_sup_of X,L & "\/" X,L = "\/" (X /\ the carrier of L),L ) by A3, A5, YELLOW_0:def 9; :: thesis: verum