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 Th11;
hence union (MaxADSF x) is anti-discrete by Th8, Th10; :: thesis: verum