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 } ;

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

{ A where A is a_partition of the carrier of T : A is closed } c= bool (bool the carrier of T)
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;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

proof

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
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;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