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

( 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