now

assume MaxADSspace A is trivial ; :: thesis: contradiction
then the carrier of (MaxADSspace A) is trivial ;
then MaxADSet A is trivial by Def19;
hence contradiction ; :: thesis: verum

end;

hence not MaxADSspace A is trivial ; :: thesis: verum