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: ( not x in RAT+ implies ex b₁ being Element of DEDEKIND_CUTS st b₁ = x )

proof

assume x in RAT+ ; :: thesis: 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 } )
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+

proof

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

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 ) )

proof

let t be Element of RAT+ ; :: thesis: ( t in IT implies ( ( 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 ) ) )
assume t in IT ; :: thesis: ( ( 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 ) )
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:101;
thus for s being Element of RAT+ st s <=' t holds
s in IT :: thesis: ex s being Element of RAT+ st
( s in IT & t < s )

proof

let s be Element of RAT+ ; :: thesis: ( s <=' t implies s in IT )
assume s <=' t ; :: thesis: s in IT
then s < r by A3, ARYTM_3:76;
hence s in IT ; :: thesis: verum

end;

take s0 ; :: thesis: ( s0 in IT & t < s0 )
thus s0 in IT by A5; :: thesis: t < s0
thus t < s0 by A4; :: thesis: verum

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:64;
take IT ; :: thesis: ex r being Element of RAT+ st
( x = r & IT = { s where s is Element of RAT+ : s < r } )
take r ; :: thesis: ( x = r & IT = { s where s is Element of RAT+ : s < r } )
thus ( x = r & IT = { s where s is Element of RAT+ : s < r } ) ; :: thesis: verum

end;

A6: x in REAL+ ;
assume not x in RAT+ ; :: thesis: ex b₁ being Element of DEDEKIND_CUTS st b₁ = x
then x in DEDEKIND_CUTS by A6, XBOOLE_0:def 3;
hence ex b₁ being Element of DEDEKIND_CUTS st b₁ = x ; :: thesis: verum