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