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

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