let X be set ; :: thesis: for D being a_partition of X
for O being closed Subset of (partition_topology D) holds O is open
let D be a_partition of X; :: thesis: for O being closed Subset of (partition_topology D) holds O is open
let O be closed Subset of (partition_topology D); :: thesis: O is open
([#] (partition_topology D)) \ O in UniCl D by PRE_TOPC:def 2, PRE_TOPC:def 3;
then A1: (X \ O) ` in UniCl D by PROB_1:def 1;
O = X /\ O by XBOOLE_1:18, XBOOLE_1:19;
hence O is open by A1, XBOOLE_1:48; :: thesis: verum