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;

now :: thesis: for A being set st A in MaxADSF x holds
{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;

then A2: {x} c= meet (MaxADSF x) by SETFAM_1:5;
{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