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_{1}[ Subset of L] means $1 in X;

set XX = { Z where Z is Subset of L : S_{1}[Z] } ;

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

"/\" ((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

set XX = { Z where Z is Subset of L : S

A2: now :: thesis: for x being object holds

( ( x in { Z where Z is Subset of L : S_{1}[Z] } implies x in X ) & ( x in X implies x in { Z where Z is Subset of L : S_{1}[Z] } ) )

"/\" ( { ("/\" (Y,L)) where Y is Subset of L : S( ( x in { Z where Z is Subset of L : S

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

_{1}[Z] }

then reconsider x9 = x as Subset of L by A1;

x9 in { Z where Z is Subset of L : S_{1}[Z] }
by A3;

hence x in { Z where Z is Subset of L : S_{1}[Z] }
; :: thesis: verum

end;hereby :: thesis: ( x in X implies x in { Z where Z is Subset of L : S_{1}[Z] } )

assume A3:
x in X
; :: thesis: x in { Z where Z is Subset of L : Sassume
x in { Z where Z is Subset of L : S_{1}[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;then ex Z being Subset of L st

( x = Z & Z in X ) ;

hence x in X ; :: thesis: verum

then reconsider x9 = x as Subset of L by A1;

x9 in { Z where Z is Subset of L : S

hence x in { Z where Z is Subset of L : S

hence "/\" ((union X),L) = "/\" ( { (inf Y) where Y is Subset of L : Y in X } ,L) by A2, TARSKI:2; :: thesis: verum