let Y be non empty TopStruct ; :: thesis: for x, y being Point of Y holds
( y in MaxADSet x iff MaxADSet y = MaxADSet x )
let x, y be Point of Y; :: thesis: ( y in MaxADSet x iff MaxADSet y = MaxADSet x )
MaxADSet y is maximal_anti-discrete by Th20;
then A1: MaxADSet y is anti-discrete ;
A2: MaxADSet x is maximal_anti-discrete by Th20;
then A3: MaxADSet x is anti-discrete ;
thus ( y in MaxADSet x implies MaxADSet y = MaxADSet x ) :: thesis: ( MaxADSet y = MaxADSet x implies y in MaxADSet x )
proof
assume y in MaxADSet x ; :: thesis: MaxADSet y = MaxADSet x
then MaxADSet x in { A where A is Subset of Y : ( A is anti-discrete & y in A ) } by A3;
then MaxADSet x c= MaxADSet y by ZFMISC_1:74;
hence MaxADSet y = MaxADSet x by A2, A1; :: thesis: verum
end;
assume A4: MaxADSet y = MaxADSet x ; :: thesis: y in MaxADSet x
{y} c= MaxADSet y by Th12;
hence y in MaxADSet x by A4, ZFMISC_1:31; :: thesis: verum