for T being non empty TopSpace holds { A where A is a_partition of the carrier of T : A is closed } is Part-Family of the carrier of T