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

let x be set ; :: 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 consider Z being Subset of L such that
A3: ( x = Z & Z in X ) ;
thus x in X by A3; :: thesis: verum

end;

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