let x, y be Element of REAL+ ; :: thesis: ( DEDEKIND_CUT x = DEDEKIND_CUT y implies x = y )
assume DEDEKIND_CUT x = DEDEKIND_CUT y ; :: thesis: x = y
then ( x <=' y & y <=' x ) by Lm20;
hence x = y by Lm21; :: thesis: verum