for X being set
for F being Subset-Family of X st {} in F & ( for A, B being set st A in F & B in F holds
A \/ B in F ) & ( for G being Subset-Family of X st G c= F holds
Intersect G in F ) holds
for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT F holds
( T is TopSpace & ( for A being Subset of T holds
( A is closed iff A in F ) ) )