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} c= meet (MaxADSF x)

proof

now

let A be set ; :: thesis: ( A in MaxADSF x implies {x} c= A )
assume A in MaxADSF x ; :: thesis: {x} c= A
then consider C being Subset of Y such that
A2: C = A and
C is anti-discrete and
A3: x in C ;
thus {x} c= A by A2, A3, ZFMISC_1:37; :: thesis: verum

end;

hence {x} c= meet (MaxADSF x) by SETFAM_1:6; :: thesis: verum

end;

meet (MaxADSF x) c= {x}

proof

( {x} is anti-discrete & x in {x} ) by Th8, TARSKI:def 1;
then {x} in MaxADSF x ;
hence meet (MaxADSF x) c= {x} by SETFAM_1:4; :: thesis: verum

end;

hence {x} = meet (MaxADSF x) by A1, XBOOLE_0:def 10; :: thesis: verum