set X = { s where s is Element of RAT+ : s < one } ;
A1: { s where s is Element of RAT+ : s < one } c= RAT+
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { s where s is Element of RAT+ : s < one } or e in RAT+ )
assume e in { s where s is Element of RAT+ : s < one } ; :: thesis: e in RAT+
then ex s being Element of RAT+ st
( s = e & s < one ) ;
hence e in RAT+ ; :: thesis: verum
end;
now :: thesis: not one in { s where s is Element of RAT+ : s < one }
assume one in { s where s is Element of RAT+ : s < one } ; :: thesis: contradiction
then ex s being Element of RAT+ st
( s = one & s < one ) ;
hence contradiction ; :: thesis: verum
end;
then A2: { s where s is Element of RAT+ : s < one } <> RAT+ ;
{} <=' one by ARYTM_3:64;
then {} < one by ARYTM_3:68;
then {} in { s where s is Element of RAT+ : s < one } ;
then reconsider X = { s where s is Element of RAT+ : s < one } as non empty Subset of RAT+ by A1;
for r being Element of RAT+ st r in X holds
( ( for s being Element of RAT+ st s <=' r holds
s in X ) & ex s being Element of RAT+ st
( s in X & r < s ) )
proof
let r be Element of RAT+ ; :: thesis: ( r in X implies ( ( for s being Element of RAT+ st s <=' r holds
s in X ) & ex s being Element of RAT+ st
( s in X & r < s ) ) )
assume r in X ; :: thesis: ( ( for s being Element of RAT+ st s <=' r holds
s in X ) & ex s being Element of RAT+ st
( s in X & r < s ) )
then A3: ex s being Element of RAT+ st
( s = r & s < one ) ;
thus for s being Element of RAT+ st s <=' r holds
s in X :: thesis: ex s being Element of RAT+ st
( s in X & r < s )
proof
let s be Element of RAT+ ; :: thesis: ( s <=' r implies s in X )
assume s <=' r ; :: thesis: s in X
then s < one by A3, ARYTM_3:67;
hence s in X ; :: thesis: verum
end;
consider s being Element of RAT+ such that
A4: r < s and
A5: s < one by A3, ARYTM_3:93;
take s ; :: thesis: ( s in X & r < s )
thus s in X by A5; :: thesis: r < s
thus r < s by A4; :: thesis: verum
end;
then X 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 ) ) } ;
hence not DEDEKIND_CUTS is empty by A2, ZFMISC_1:56; :: thesis: verum