let Y be non empty TopStruct ; :: thesis: for x being Point of Y holds MaxADSet x is maximal_anti-discrete

let x be Point of Y; :: thesis: MaxADSet x is maximal_anti-discrete

A1: for D being Subset of Y st D is anti-discrete & MaxADSet x c= D holds

MaxADSet x = D

hence MaxADSet x is maximal_anti-discrete by A1; :: thesis: verum

let x be Point of Y; :: thesis: MaxADSet x is maximal_anti-discrete

A1: for D being Subset of Y st D is anti-discrete & MaxADSet x c= D holds

MaxADSet x = D

proof

MaxADSet x is anti-discrete
by Th13;
let D be Subset of Y; :: thesis: ( D is anti-discrete & MaxADSet x c= D implies MaxADSet x = D )

assume A2: D is anti-discrete ; :: thesis: ( not MaxADSet x c= D or MaxADSet x = D )

assume A3: MaxADSet x c= D ; :: thesis: MaxADSet x = D

{x} c= MaxADSet x by Th12;

then {x} c= D by A3;

then x in D by ZFMISC_1:31;

then D c= MaxADSet x by A2, Th19;

hence MaxADSet x = D by A3; :: thesis: verum

end;assume A2: D is anti-discrete ; :: thesis: ( not MaxADSet x c= D or MaxADSet x = D )

assume A3: MaxADSet x c= D ; :: thesis: MaxADSet x = D

{x} c= MaxADSet x by Th12;

then {x} c= D by A3;

then x in D by ZFMISC_1:31;

then D c= MaxADSet x by A2, Th19;

hence MaxADSet x = D by A3; :: thesis: verum

hence MaxADSet x is maximal_anti-discrete by A1; :: thesis: verum