reconsider ct = { the carrier of T} as a_partition of the carrier of T by EQREL_1:39;
set F = { A where A is a_partition of the carrier of T : A is closed } ;
for A being Subset of T st A in ct holds
A is closed by TARSKI:def 1;
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 Th3; :: thesis: verum