let C be complete Lattice; :: thesis: for X being set st X c= bool the carrier of C holds
"\/" (union X),C = "\/" { ("\/" Y) where Y is Subset of C : Y in X } ,C
let X be set ; :: thesis: ( X c= bool the carrier of C implies "\/" (union X),C = "\/" { ("\/" Y) where Y is Subset of C : Y in X } ,C )
set Z = { ("\/" Y) where Y is Subset of C : Y in X } ;
{ ("\/" Y) where Y is Subset of C : Y in X } is_less_than "\/" (union X),C

proof

let a be Element of C; :: according to LATTICE3:def 17 :: thesis: ( a in { ("\/" Y) where Y is Subset of C : Y in X } implies a [= "\/" (union X),C )
assume a in { ("\/" Y) where Y is Subset of C : Y in X } ; :: thesis: a [= "\/" (union X),C
then consider Y being Subset of C such that
A1: ( a = "\/" Y & Y in X ) ;
Y c= union X by A1, ZFMISC_1:92;
hence a [= "\/" (union X),C by A1, Th46; :: thesis: verum

end;

then A2: "\/" { ("\/" Y) where Y is Subset of C : Y in X } ,C [= "\/" (union X),C by Def21;
set V = { a where a is Element of C : ex b being Element of C st
( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) } ;
assume A3: X c= bool the carrier of C ; :: thesis: "\/" (union X),C = "\/" { ("\/" Y) where Y is Subset of C : Y in X } ,C
union X c= { a where a is Element of C : ex b being Element of C st
( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union X or x in { a where a is Element of C : ex b being Element of C st
( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) } )
assume x in union X ; :: thesis: x in { a where a is Element of C : ex b being Element of C st
( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) }
then consider Y being set such that
A4: ( x in Y & Y in X ) by TARSKI:def 4;
reconsider Y = Y as Subset of C by A3, A4;
reconsider a = x as Element of C by A3, A4;
( a [= "\/" Y & "\/" Y in { ("\/" Y) where Y is Subset of C : Y in X } ) by A4, Th38;
hence x in { a where a is Element of C : ex b being Element of C st
( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) } ; :: thesis: verum

end;

then "\/" (union X),C [= "\/" { a where a is Element of C : ex b being Element of C st
( a [= b & b in { ("\/" Y) where Y is Subset of C : Y in X } ) } ,C by Th46;
then "\/" (union X),C [= "\/" { ("\/" Y) where Y is Subset of C : Y in X } ,C by Th47;
hence "\/" (union X),C = "\/" { ("\/" Y) where Y is Subset of C : Y in X } ,C by A2, LATTICES:26; :: thesis: verum