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 and
A2: Y in X ;
Y c= union X by A2, ZFMISC_1:92;
hence a [= "\/" (union X),C by A1, Th46; :: thesis: verum

end;

then A3: "\/" { ("\/" 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 A4: 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
A5: x in Y and
A6: Y in X by TARSKI:def 4;
reconsider Y = Y as Subset of C by A4, A6;
reconsider a = x as Element of C by A4, A5, A6;
A7: a [= "\/" Y by A5, Th38;
"\/" Y in { ("\/" Y) where Y is Subset of C : Y in X } by A6;
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 } ) } by A7; :: 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 A3, LATTICES:26; :: thesis: verum