0 in {0 } by TARSKI:def 1;
then [0 ,1] in [:{0 },NAT :] by ZFMISC_1:106;
then A1: [0 ,1] in NAT \/ [:{0 },NAT :] by XBOOLE_0:def 3;
[0 ,1] <> [0 ,0 ] by ZFMISC_1:33;
then not [0 ,1] in {[0 ,0 ]} by TARSKI:def 1;
then A2: [0 ,1] in INT by A1, XBOOLE_0:def 5;
not [0 ,1] in NAT by ARYTM_3:38;
hence NAT c< INT by A2, Lm5, XBOOLE_0:def 8; :: thesis: verum