theorem Th1: :: T_1TOPSP:1

for T being non empty TopSpace
for A being non empty a_partition of the carrier of T
for y being Subset of (space A) holds (Proj A) " y = union y