let B be set ; :: thesis: ( B in DEDEKIND_CUTS & B <> {} implies ex r being Element of RAT+ st
( r in B & r <> {} ) )
assume that
A1: B in DEDEKIND_CUTS and
A2: B <> {} ; :: thesis: ex r being Element of RAT+ st
( r in B & r <> {} )
B 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 ) ) } by A1;
then consider A being Subset of RAT+ such that
A3: B = A and
A4: 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 ) ) ;
reconsider A = A as non empty Subset of RAT+ by A2, A3;
consider r0 being Element of RAT+ such that
A5: r0 in A by SUBSET_1:4;
consider r1 being Element of RAT+ such that
A6: r1 in A and
A7: r0 < r1 by A4, A5;
A8: ( r1 <> {} or r0 <> {} ) by A7;
for r, s being Element of RAT+ st r in A & s <=' r holds
s in A by A4;
then consider r1, r2, r3 being Element of RAT+ such that
A9: ( r1 in A & r2 in A ) and
r3 in A and
A10: r1 <> r2 and
r2 <> r3 and
r3 <> r1 by A5, A6, A8, ARYTM_3:75;
( r1 <> {} or r2 <> {} ) by A10;
hence ex r being Element of RAT+ st
( r in B & r <> {} ) by A3, A9; :: thesis: verum