theorem Th7: :: TOPGEN_3:7

for X being set
for c being Function of (bool X),(bool X) st c . {} = {} & ( for A being Subset of X holds A c= c . A ) & ( for A, B being Subset of X holds c . (A \/ B) = (c . A) \/ (c . B) ) & ( for A being Subset of X holds c . (c . A) = c . A ) holds
for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT (rng c) holds
( T is TopSpace & ( for A being Subset of T holds Cl A = c . A ) )