A c= MaxADSet A by Th32;
hence not MaxADSet A is trivial ; :: thesis: verum