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

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