now :: thesis: not MaxADSspace A is proper
assume A1: MaxADSspace A is proper ; :: thesis: contradiction
the carrier of (MaxADSspace A) = MaxADSet A by Def18;
hence contradiction by A1, TEX_2:8; :: thesis: verum
end;
hence not MaxADSspace A is proper ; :: thesis: verum