for T being non empty TopSpace
for x being Element of (InclPoset the topology of T)
for X being Subset of T st x = X holds
( x is compact iff X is compact )