let T be non empty TopSpace; :: thesis: { A where A is a_partition of the carrier of T : A is closed } is Part-Family of the carrier of T
set S = { A where A is a_partition of the carrier of T : A is closed } ;
A1: { A where A is a_partition of the carrier of T : A is closed } c= bool (bool the carrier of T)

proof

let B be set ; :: according to TARSKI:def 3 :: thesis: ( not B in { A where A is a_partition of the carrier of T : A is closed } or B in bool (bool the carrier of T) )
assume B in { A where A is a_partition of the carrier of T : A is closed } ; :: thesis: B in bool (bool the carrier of T)
then consider A being a_partition of the carrier of T such that
A2: B = A and
A is closed ;
thus B in bool (bool the carrier of T) by A2; :: thesis: verum

end;

now

let B be set ; :: thesis: ( B in { A where A is a_partition of the carrier of T : A is closed } implies B is a_partition of the carrier of T )
assume B in { A where A is a_partition of the carrier of T : A is closed } ; :: thesis: B is a_partition of the carrier of T
then consider A being a_partition of the carrier of T such that
A3: B = A and
A is closed ;
thus B is a_partition of the carrier of T by A3; :: thesis: verum

end;

hence { A where A is a_partition of the carrier of T : A is closed } is Part-Family of the carrier of T by A1, EQREL_1:def 10; :: thesis: verum