let r, s be Element of RAT+ ; :: thesis: for B being set st B in DEDEKIND_CUTS & r in B & s <=' r holds
s in B
let B be set ; :: thesis: ( B in DEDEKIND_CUTS & r in B & s <=' r implies s in B )
assume that
A1: B in DEDEKIND_CUTS and
A2: ( r in B & s <=' r ) ; :: thesis: s in B
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 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 s in B by A2; :: thesis: verum