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 S₁[ set ] means $1 in X;
set XX = { Z where Z is Subset of L : S₁[Z] } ;

A2: now :: thesis: for x being object holds
( ( x in { Z where Z is Subset of L : S₁[Z] } implies x in X ) & ( x in X implies x in { Z where Z is Subset of L : S₁[Z] } ) )

let x be object ; :: thesis: ( ( x in { Z where Z is Subset of L : S₁[Z] } implies x in X ) & ( x in X implies x in { Z where Z is Subset of L : S₁[Z] } ) )

hereby :: thesis: ( x in X implies x in { Z where Z is Subset of L : S₁[Z] } )

assume x in { Z where Z is Subset of L : S₁[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 : S₁[Z] }
then reconsider x9 = x as Subset of L by A1;
x9 in { Z where Z is Subset of L : S₁[Z] } by A3;
hence x in { Z where Z is Subset of L : S₁[Z] } ; :: thesis: verum

end;

"\/" ( { ("\/" (Y,L)) where Y is Subset of L : S₁[Y] } ,L) = "\/" ((union { Z where Z is Subset of L : S₁[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