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