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