A = the carrier of Y by SUBSET_1:def 6;
then the carrier of Y c= MaxADSet A by Th32;
then MaxADSet A = the carrier of Y ;
hence not MaxADSet A is proper ; :: thesis: verum