take id NAT ; :: thesis: ( not id NAT is empty & id NAT is NAT -defined )
thus ( not id NAT is empty & id NAT is NAT -defined ) ; :: thesis: verum