for X being non empty TopSpace
for A being Subset of X holds
( A is open iff TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to A ) by Th92;