let L be complete LATTICE; :: thesis: for X being set st X c= bool the carrier of L holds
"\/" ((union X),L) = "\/" ( { (sup Y) where Y is Subset of L : Y in X } ,L)
let X be set ; :: thesis: ( X c= bool the carrier of L implies "\/" ((union X),L) = "\/" ( { (sup Y) where Y is Subset of L : Y in X } ,L) )
assume A1: X c= bool the carrier of L ; :: thesis: "\/" ((union X),L) = "\/" ( { (sup Y) where Y is Subset of L : Y in X } ,L)
defpred S1[ set ] means $1 in X;
set XX = { Z where Z is Subset of L : S1[Z] } ;
A2: now :: thesis: for x being object holds
( ( x in { Z where Z is Subset of L : S1[Z] } implies x in X ) & ( x in X implies x in { Z where Z is Subset of L : S1[Z] } ) )
let x be object ; :: thesis: ( ( x in { Z where Z is Subset of L : S1[Z] } implies x in X ) & ( x in X implies x in { Z where Z is Subset of L : S1[Z] } ) )
hereby :: thesis: ( x in X implies x in { Z where Z is Subset of L : S1[Z] } )
assume x in { Z where Z is Subset of L : S1[Z] } ; :: thesis: x in X
then ex Z being Subset of L st
( x = Z & Z in X ) ;
hence x in X ; :: thesis: verum
end;
assume A3: x in X ; :: thesis: x in { Z where Z is Subset of L : S1[Z] }
then reconsider x9 = x as Subset of L by A1;
x9 in { Z where Z is Subset of L : S1[Z] } by A3;
hence x in { Z where Z is Subset of L : S1[Z] } ; :: thesis: verum
end;
"\/" ( { ("\/" (Y,L)) where Y is Subset of L : S1[Y] } ,L) = "\/" ((union { Z where Z is Subset of L : S1[Z] } ),L) from YELLOW_3:sch 5();
 hence "\/" ((union X),L) = "\/" ( { (sup Y) where Y is Subset of L : Y in X } ,L) by A2, TARSKI:2; :: thesis: verum