let X be set ; :: thesis: for D being a_partition of X holds { (union P) where P is Subset of D : verum } = UniCl D
let D be a_partition of X; :: thesis: { (union P) where P is Subset of D : verum } = UniCl D
set F = { (union P) where P is Subset of D : verum } ;
thus { (union P) where P is Subset of D : verum } c= UniCl D :: according to XBOOLE_0:def 10 :: thesis: UniCl D c= { (union P) where P is Subset of D : verum }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (union P) where P is Subset of D : verum } or x in UniCl D )
assume x in { (union P) where P is Subset of D : verum } ; :: thesis: x in UniCl D
then consider P being Subset of D such that
A2: x = union P ;
( P c= D & D c= bool X ) ;
then P c= bool X ;
then reconsider Y = P as Subset-Family of X ;
( Y c= D & union Y = union P ) ;
hence x in UniCl D by A2, CANTOR_1:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UniCl D or x in { (union P) where P is Subset of D : verum } )
assume x in UniCl D ; :: thesis: x in { (union P) where P is Subset of D : verum }
then consider Y being Subset-Family of X such that
A3: Y c= D and
A4: x = union Y by CANTOR_1:def 1;
reconsider P = Y as Subset of D by A3;
x = union P by A4;
hence x in { (union P) where P is Subset of D : verum } ; :: thesis: verum