set F = { A where A is a_partition of the carrier of T : A is closed } ;
reconsider ct = {the carrier of T} as a_partition of the carrier of T by EQREL_1:48;
for A being Subset of T st A in ct holds
A is closed

proof

let A be Subset of T; :: thesis: ( A in ct implies A is closed )
assume A in ct ; :: thesis: A is closed
then A = [#] T by TARSKI:def 1;
hence A is closed ; :: thesis: verum

end;

then ct is closed by TOPS_2:def 2;
then ct in { A where A is a_partition of the carrier of T : A is closed } ;
hence { A where A is a_partition of the carrier of T : A is closed } is non empty Part-Family of the carrier of T by Th11; :: thesis: verum