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

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