set D = MaxADSet x;
set Y0 = Y | (MaxADSet x);
take Y | (MaxADSet x) ; :: thesis: the carrier of (Y | (MaxADSet x)) = MaxADSet x
MaxADSet x = [#] (Y | (MaxADSet x)) by PRE_TOPC:def 5;
hence the carrier of (Y | (MaxADSet x)) = MaxADSet x ; :: thesis: verum