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