not MaxADSet A is trivial ;
hence not MaxADSspace A is trivial by Def18; :: thesis: verum