( NAT c< ExtNAT & ExtNAT c< ExtREAL )