now

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