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