let L be non empty RelStr ; ( ( 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
; for X being set holds
( ex_sup_of X,L & "\/" (X,L) = "\/" ((X /\ the carrier of L),L) )
let X be set ; ( 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)
A5:
for b being Element of L st X is_<=_than b holds
"\/" ((X /\ the carrier of L),L) <= b
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; verum