theorem :: TEX_4:77

for X being non empty TopSpace
for X0 being non empty open SubSpace of X
for x being Point of X st x is Point of X0 holds
MaxADSspace x is SubSpace of X0