take NAT --> {} ; :: thesis: NAT --> {} is D -defined
thus NAT --> {} is D -defined by RELAT_1:171; :: thesis: verum