now :: thesis: not MaxADSspace A is proper

hence
not MaxADSspace A is proper
; :: thesis: verumassume 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;the carrier of (MaxADSspace A) = MaxADSet A by Def18;

hence contradiction by A1, TEX_2:8; :: thesis: verum