A = the carrier of Y by SUBSET_1:def 7;
then ( the carrier of Y c= MaxADSet A & MaxADSet A c= the carrier of Y ) 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