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