A = the carrier of Y by SUBSET_1:def 7;
then the carrier of Y c= MaxADSet A by Th34;
then MaxADSet A = the carrier of Y by XBOOLE_0:def 10;
hence not MaxADSet A is proper by SUBSET_1:def 7; :: thesis: verum