let Y be non empty TopStruct ; :: thesis: for x being Point of Y holds {x} = meet (MaxADSF x)

let x be Point of Y; :: thesis: {x} = meet (MaxADSF x)

A1: x in {x} by TARSKI:def 1;

{x} is anti-discrete by Th6;

then {x} in MaxADSF x by A1;

then meet (MaxADSF x) c= {x} by SETFAM_1:3;

hence {x} = meet (MaxADSF x) by A2; :: thesis: verum

let x be Point of Y; :: thesis: {x} = meet (MaxADSF x)

A1: x in {x} by TARSKI:def 1;

now :: thesis: for A being set st A in MaxADSF x holds

{x} c= A

then A2:
{x} c= meet (MaxADSF x)
by SETFAM_1:5;{x} c= A

let A be set ; :: thesis: ( A in MaxADSF x implies {x} c= A )

assume A in MaxADSF x ; :: thesis: {x} c= A

then ex C being Subset of Y st

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

hence {x} c= A by ZFMISC_1:31; :: thesis: verum

end;assume A in MaxADSF x ; :: thesis: {x} c= A

then ex C being Subset of Y st

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

hence {x} c= A by ZFMISC_1:31; :: thesis: verum

{x} is anti-discrete by Th6;

then {x} in MaxADSF x by A1;

then meet (MaxADSF x) c= {x} by SETFAM_1:3;

hence {x} = meet (MaxADSF x) by A2; :: thesis: verum