take {} ; :: thesis: ( {} is finite & {} is NAT -defined )
thus {} is finite ; :: thesis: {} is NAT -defined
thus dom {} c= NAT ; :: according to RELAT_1:def 18 :: thesis: verum