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) by Th11;
hence {x} c= union (MaxADSF x) by SETFAM_1:2; :: thesis: verum