[:{0 },NAT :] c= [:{0 },RAT+ :] by Lm1, ZFMISC_1:118;
then NAT \/ [:{0 },NAT :] c= RAT+ \/ [:{0 },RAT+ :] by Lm1, XBOOLE_1:13;
hence INT c= RAT by XBOOLE_1:33; :: thesis: verum