let Y be non empty TopStruct ; :: thesis: for x, y being Point of Y holds
( MaxADSet x misses MaxADSet y or MaxADSet x = MaxADSet y )
let x, y be Point of Y; :: thesis: ( MaxADSet x misses MaxADSet y or MaxADSet x = MaxADSet y )
assume (MaxADSet x) /\ (MaxADSet y) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: MaxADSet x = MaxADSet y
then consider a being object such that
A1: a in (MaxADSet x) /\ (MaxADSet y) by XBOOLE_0:def 1;
reconsider a = a as Point of Y by A1;
a in MaxADSet x by A1, XBOOLE_0:def 4;
then A2: MaxADSet a = MaxADSet x by Th21;
a in MaxADSet y by A1, XBOOLE_0:def 4;
hence MaxADSet x = MaxADSet y by A2, Th21; :: thesis: verum