reconsider D = {y} as non empty Subset of Y ;
set Y0 = Y | D;
take Y | D ; :: thesis: the carrier of (Y | D) = {y}
D = [#] (Y | D) by PRE_TOPC:def 5;
hence the carrier of (Y | D) = {y} ; :: thesis: verum