A1: MaxADSet x is maximal_anti-discrete by Th20;
MaxADSet x = the carrier of (MaxADSspace x) by Def17;
hence MaxADSspace x is maximal_anti-discrete by A1, Th72; :: thesis: verum