let Y be non empty TopStruct ; :: thesis: for x being Point of Y holds {x} c= union (MaxADSF x)
let x be Point of Y; :: thesis: {x} c= union (MaxADSF x)
( {x} = meet (MaxADSF x) & meet (MaxADSF x) c= union (MaxADSF x) ) by Th13, SETFAM_1:3;
hence {x} c= union (MaxADSF x) ; :: thesis: verum