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 10;
hence MaxADSet x = the carrier of (Y | (MaxADSet x)) ; :: thesis: verum