theorem Th53: :: TEX_4:53

for X being non empty TopSpace
for x, y being Point of X holds
( MaxADSet x misses MaxADSet y iff ( ex V being Subset of X st
( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st
( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) )