let x, y be Element of REAL+ ; :: thesis: ( DEDEKIND_CUT x c= DEDEKIND_CUT y implies x <=' y )
assume A1: DEDEKIND_CUT x c= DEDEKIND_CUT y ; :: thesis: x <=' y

per cases ( ( x = {} & not y in RAT+ ) or y = {} or ( x in RAT+ & y in RAT+ ) or ( x in RAT+ & not y in RAT+ & x <> {} ) or ( not x in RAT+ & y in RAT+ & y <> {} ) or ( not x in RAT+ & not y in RAT+ ) ) ;

suppose that A2: x = {} and
A3: not y in RAT+ ; :: thesis: x <=' y

A4: DEDEKIND_CUT y = y by A3, Def3;
y <> {} by A3;
then x in y by A2, A4, Lm17;
hence x <=' y by A2, A3, Def5; :: thesis: verum

end;

suppose A5: y = {} ; :: thesis: x <=' y

then DEDEKIND_CUT y = {} by Lm10;
then DEDEKIND_CUT x = {} by A1;
then x = {} by Lm10;
hence x <=' y by A5; :: thesis: verum

end;

suppose that A6: x in RAT+ and
A7: y in RAT+ ; :: thesis: x <=' y

consider rx being Element of RAT+ such that
A8: x = rx and
A9: DEDEKIND_CUT x = { s where s is Element of RAT+ : s < rx } by A6, Def3;
consider ry being Element of RAT+ such that
A10: y = ry and
A11: DEDEKIND_CUT y = { s where s is Element of RAT+ : s < ry } by A7, Def3;
assume y < x ; :: thesis: contradiction
then ry < rx by A8, A10, Lm14;
then ry in DEDEKIND_CUT x by A9;
then ry in DEDEKIND_CUT y by A1;
then ex s being Element of RAT+ st
( s = ry & s < ry ) by A11;
hence contradiction ; :: thesis: verum

end;

suppose that A12: x in RAT+ and
A13: not y in RAT+ and
A14: x <> {} ; :: thesis: x <=' y

consider rx being Element of RAT+ such that
A15: x = rx and
A16: DEDEKIND_CUT x = { s where s is Element of RAT+ : s < rx } by A12, Def3;
A17: DEDEKIND_CUT x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A14, A15, A16;
A18: DEDEKIND_CUT y = y by A13, Def3;
then DEDEKIND_CUT x <> y by A13, A17, Lm19;
then not DEDEKIND_CUT y c= DEDEKIND_CUT x by A1, A18, XBOOLE_0:def 10;
then consider r0 being Element of RAT+ such that
A19: r0 in y and
A20: not r0 in DEDEKIND_CUT x by A18, SUBSET_1:7;
rx <=' r0 by A16, A20;
then x in y by A15, A18, A19, Lm16;
hence x <=' y by A12, A13, Def5; :: thesis: verum

end;

suppose that A21: not x in RAT+ and
A22: y in RAT+ and
A23: y <> {} ; :: thesis: x <=' y

consider ry being Element of RAT+ such that
A24: y = ry and
A25: DEDEKIND_CUT y = { s where s is Element of RAT+ : s < ry } by A22, Def3;
A26: DEDEKIND_CUT y in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A23, A24, A25;
A27: DEDEKIND_CUT x = x by A21, Def3;
then not x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A21, Lm19;
then not DEDEKIND_CUT y c= DEDEKIND_CUT x by A1, A26, A27, XBOOLE_0:def 10;
then consider r0 being Element of RAT+ such that
A28: r0 in DEDEKIND_CUT y and
A29: not r0 in x by A27, SUBSET_1:7;
ex s being Element of RAT+ st
( s = r0 & s < ry ) by A25, A28;
then not y in x by A24, A27, A29, Lm16;
hence x <=' y by A21, A22, Def5; :: thesis: verum

end;

suppose that A30: not x in RAT+ and
A31: not y in RAT+ ; :: thesis: x <=' y

( x = DEDEKIND_CUT x & y = DEDEKIND_CUT y ) by A30, A31, Def3;
hence x <=' y by A1, A30, A31, Def5; :: thesis: verum

end;

end;