let Y be non empty TopStruct ; :: thesis: for x being Point of Y holds union (MaxADSF x) is anti-discrete
let x be Point of Y; :: thesis: union (MaxADSF x) is anti-discrete
{x} = meet (MaxADSF x) by Th13;
hence union (MaxADSF x) is anti-discrete by Th10, Th12; :: thesis: verum