thus ( x in RAT+ implies ex IT being Element of DEDEKIND_CUTS ex r being Element of RAT+ st
( x = r & IT = { s where s is Element of RAT+ : s < r } ) ) :: thesis:

assume x in RAT+ ; :: thesis:
then reconsider r = x as Element of RAT+ ;
set IT = { s where s is Element of RAT+ : s < r } ;
A1: { s where s is Element of RAT+ : s < r } c= RAT+

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in { s where s is Element of RAT+ : s < r } ; :: thesis:
then ex s being Element of RAT+ st
( s = e & s < r ) ;
hence e in RAT+ ; :: thesis:

end;

for s being Element of RAT+ holds
( not s = r or not s < r ) ;
then not r in { s where s is Element of RAT+ : s < r } ;
then A2: { s where s is Element of RAT+ : s < r } <> RAT+ ;
reconsider IT = { s where s is Element of RAT+ : s < r } as Subset of RAT+ by A1;
for t being Element of RAT+ st t in IT holds
( ( for s being Element of RAT+ st s <=' t holds
s in IT ) & ex s being Element of RAT+ st
( s in IT & t < s ) )

let t be Element of RAT+ ; :: thesis:
assume t in IT ; :: thesis:
then A3: ex s being Element of RAT+ st
( t = s & s < r ) ;
then consider s0 being Element of RAT+ such that
A4: t < s0 and
A5: s0 < r by ARYTM_3:93;
thus for s being Element of RAT+ st s <=' t holds
s in IT :: thesis:

end;

take s0 ; :: thesis:
thus s0 in IT by A5; :: thesis:
thus t < s0 by A4; :: thesis:

end;

then IT in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ;
then reconsider IT = IT as Element of DEDEKIND_CUTS by A2, ZFMISC_1:56;
take IT ; :: thesis:
take r ; :: thesis:
thus ( x = r & IT = { s where s is Element of RAT+ : s < r } ) ; :: thesis:

end;