let L be complete LATTICE; :: thesis: for X being set st X c= bool the carrier of L holds
"/\" ((union X),L) = "/\" ( { (inf 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) = "/\" ( { (inf Y) where Y is Subset of L : Y in X } ,L) )
assume A1: X c= bool the carrier of L ; :: thesis: "/\" ((union X),L) = "/\" ( { (inf Y) where Y is Subset of L : Y in X } ,L)
defpred S₁[ Subset of L] 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 3();
hence "/\" ((union X),L) = "/\" ( { (inf Y) where Y is Subset of L : Y in X } ,L) by A2, TARSKI:2; :: thesis: verum