assume RAT+ meets { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; :: thesis: contradiction
then consider e being object such that
A1: e in RAT+ and
A2: e in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by XBOOLE_0:3;
reconsider e = e as set by TARSKI:1;
consider t being Element of RAT+ such that
A3: e = { s where s is Element of RAT+ : s < t } and
A4: t <> {} by A2;
{} <=' t by ARYTM_3:64;
then {} < t by A4, ARYTM_3:68;
then A5: {} in e by A3;
e c= RAT+

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in e or u in RAT+ )
assume u in e ; :: thesis: u in RAT+
then ex s being Element of RAT+ st
( s = u & s < t ) by A3;
hence u in RAT+ ; :: thesis: verum

end;

then reconsider e = e as non empty Subset of RAT+ by A5;
consider s being Element of RAT+ such that
A6: s in e and
A7: for r being Element of RAT+ st r in e holds
r <=' s by A1, ARYTM_3:91;
ex r being Element of RAT+ st
( r = s & r < t ) by A3, A6;
then consider r being Element of RAT+ such that
A8: s < r and
A9: r < t by ARYTM_3:93;
r in e by A3, A9;
hence contradiction by A7, A8; :: thesis: verum