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: now :: thesis: for B being set st B in { A where A is a_partition of the carrier of T : A is closed } holds
B is a_partition of the carrier of T
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 ex A being a_partition of the carrier of T st
( B = A & A is closed ) ;
hence B is a_partition of the carrier of T ; :: thesis: verum
end;
{ 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 object ; :: 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 ex A being a_partition of the carrier of T st
( B = A & A is closed ) ;
hence B in bool (bool the carrier of T) ; :: 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 7; :: thesis: verum