let x, y be Element of REAL+ ; :: thesis: ( x <=' y implies DEDEKIND_CUT x c= DEDEKIND_CUT y )
assume A1: x <=' y ; :: thesis: DEDEKIND_CUT x c= DEDEKIND_CUT y
assume A2: not DEDEKIND_CUT x c= DEDEKIND_CUT y ; :: thesis: contradiction
( DEDEKIND_CUT 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 ) ) } & DEDEKIND_CUT y 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 XBOOLE_0:def 5;
then DEDEKIND_CUT y c= DEDEKIND_CUT x by A2, Lm13;
then y <=' x by Lm20;
hence contradiction by A1, A2, Lm21; :: thesis: verum