let r be Element of RAT+ ; :: thesis: for B being set st B in DEDEKIND_CUTS & r in B holds
ex s being Element of RAT+ st
( s in B & r < s )
let B be set ; :: thesis: ( B in DEDEKIND_CUTS & r in B implies ex s being Element of RAT+ st
( s in B & r < s ) )
assume B in DEDEKIND_CUTS ; :: thesis: ( not r in B or ex s being Element of RAT+ st
( s in B & r < s ) )
then 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 ) ) } ;
then ex A being Subset of RAT+ st
( B = A & ( for t being Element of RAT+ st t in A holds
( ( for s being Element of RAT+ st s <=' t holds
s in A ) & ex s being Element of RAT+ st
( s in A & t < s ) ) ) ) ;
hence ( not r in B or ex s being Element of RAT+ st
( s in B & r < s ) ) ; :: thesis: verum