let Y be non empty TopStruct ; :: thesis: for x being Point of Y holds MaxADSF x is anti-discrete-set-family

let x be Point of Y; :: thesis: MaxADSF x is anti-discrete-set-family

let x be Point of Y; :: thesis: MaxADSF x is anti-discrete-set-family

now :: thesis: for A being Subset of Y st A in MaxADSF x holds

A is anti-discrete

hence
MaxADSF x is anti-discrete-set-family
; :: thesis: verumA is anti-discrete

let A be Subset of Y; :: thesis: ( A in MaxADSF x implies A is anti-discrete )

assume A in MaxADSF x ; :: thesis: A is anti-discrete

then ex C being Subset of Y st

( C = A & C is anti-discrete & x in C ) ;

hence A is anti-discrete ; :: thesis: verum

end;assume A in MaxADSF x ; :: thesis: A is anti-discrete

then ex C being Subset of Y st

( C = A & C is anti-discrete & x in C ) ;

hence A is anti-discrete ; :: thesis: verum