for X being non empty TopSpace
for X0 being maximal_Kolmogorov_subspace of X
for G being Subset of X holds
( G is open iff ( G = MaxADSet G & ex G0 being Subset of X0 st
( G0 is open & G0 = G /\ the carrier of X0 ) ) )