let L be non empty RelStr ; :: thesis: for X being set st ( ex_sup_of X,L or ex_sup_of X /\ the carrier of L,L ) holds
"\/" (X,L) = "\/" ((X /\ the carrier of L),L)
let X be set ; :: thesis: ( ( ex_sup_of X,L or ex_sup_of X /\ the carrier of L,L ) implies "\/" (X,L) = "\/" ((X /\ the carrier of L),L) )
set Y = X /\ the carrier of L;
assume A1: ( ex_sup_of X,L or ex_sup_of X /\ the carrier of L,L ) ; :: thesis: "\/" (X,L) = "\/" ((X /\ the carrier of L),L)
for x being Element of L holds
( x is_>=_than X iff x is_>=_than X /\ the carrier of L ) by Th5;
hence "\/" (X,L) = "\/" ((X /\ the carrier of L),L) by A1, Th47; :: thesis: verum