let X be non empty set ; :: thesis: for D being a_partition of X holds capOpCl (partition_topology D) = UniCl D
let D be a_partition of X; :: thesis: capOpCl (partition_topology D) = UniCl D
set Y = { (A /\ B) where A, B is Subset of (partition_topology D) : ( A is open & B is closed ) } ;
A1: { (A /\ B) where A, B is Subset of (partition_topology D) : ( A is open & B is closed ) } c= UniCl D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (A /\ B) where A, B is Subset of (partition_topology D) : ( A is open & B is closed ) } or x in UniCl D )
assume x in { (A /\ B) where A, B is Subset of (partition_topology D) : ( A is open & B is closed ) } ; :: thesis: x in UniCl D
then consider A, B being Subset of (partition_topology D) such that
A2: x = A /\ B and
A3: A is open and
A4: B is closed ;
B is open by A4, Th19;
hence x in UniCl D by A2, A3, FINSUB_1:def 2; :: thesis: verum

end;

UniCl D c= { (A /\ B) where A, B is Subset of (partition_topology D) : ( A is open & B is closed ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UniCl D or x in { (A /\ B) where A, B is Subset of (partition_topology D) : ( A is open & B is closed ) } )
assume A5: x in UniCl D ; :: thesis: x in { (A /\ B) where A, B is Subset of (partition_topology D) : ( A is open & B is closed ) }
then reconsider y = x as Subset of (partition_topology D) ;
X in UniCl D by Th15;
then reconsider XX = X as Subset of (partition_topology D) ;
A6: y = y /\ X by XBOOLE_1:18, XBOOLE_1:19;
( y is open & XX is closed ) by A5;
hence x in { (A /\ B) where A, B is Subset of (partition_topology D) : ( A is open & B is closed ) } by A6; :: thesis: verum

end;

hence capOpCl (partition_topology D) = UniCl D by A1; :: thesis: verum