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