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
( DEDEKIND_CUT y = y & y <> {} ) by A3, Def3;
then x in y by A2, Lm17;
hence x <=' y by A2, A3, Def5; :: thesis: verum
end;
suppose A4: y = {} ; :: thesis: x <=' y
then DEDEKIND_CUT y = {} by Lm10;
then DEDEKIND_CUT x = {} by A1;
then x = {} by Lm10;
hence x <=' y by A4; :: thesis: verum
end;
suppose that A5: x in RAT+ and
A6: y in RAT+ ; :: thesis: x <=' y
consider ry being Element of RAT+ such that
A7: y = ry and
A8: DEDEKIND_CUT y = { s where s is Element of RAT+ : s < ry } by A6, Def3;
consider rx being Element of RAT+ such that
A9: x = rx and
A10: DEDEKIND_CUT x = { s where s is Element of RAT+ : s < rx } by A5, Def3;
assume y < x ; :: thesis: contradiction
then ry < rx by A9, A7, Lm14;
then ry in DEDEKIND_CUT x by A10;
then ry in DEDEKIND_CUT y by A1;
then ex s being Element of RAT+ st
( s = ry & s < ry ) by A8;
hence contradiction ; :: thesis: verum
end;
suppose that A11: x in RAT+ and
A12: not y in RAT+ and
A13: x <> {} ; :: thesis: x <=' y
A14: DEDEKIND_CUT y = y by A12, Def3;
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 A11, Def3;
DEDEKIND_CUT x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A13, A15, A16;
then DEDEKIND_CUT x <> y by A12, A14, Lm19;
then not DEDEKIND_CUT y c= DEDEKIND_CUT x by A1, A14;
then consider r0 being Element of RAT+ such that
A17: r0 in y and
A18: not r0 in DEDEKIND_CUT x by A14;
rx <=' r0 by A16, A18;
then x in y by A15, A14, A17, Lm16;
hence x <=' y by A11, A12, Def5; :: thesis: verum
end;
suppose that A19: not x in RAT+ and
A20: y in RAT+ and
A21: y <> {} ; :: thesis: x <=' y
consider ry being Element of RAT+ such that
A22: y = ry and
A23: DEDEKIND_CUT y = { s where s is Element of RAT+ : s < ry } by A20, Def3;
A24: DEDEKIND_CUT y in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A21, A22, A23;
A25: DEDEKIND_CUT x = x by A19, Def3;
then not x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A19, Lm19;
then not DEDEKIND_CUT y c= DEDEKIND_CUT x by A1, A24, A25, XBOOLE_0:def 10;
then consider r0 being Element of RAT+ such that
A26: r0 in DEDEKIND_CUT y and
A27: not r0 in x by A25;
ex s being Element of RAT+ st
( s = r0 & s < ry ) by A23, A26;
then not y in x by A22, A25, A27, Lm16;
hence x <=' y by A19, A20, Def5; :: thesis: verum
end;
suppose A28: ( not x in RAT+ & not y in RAT+ ) ; :: thesis: x <=' y
( x = DEDEKIND_CUT x & y = DEDEKIND_CUT y ) by A28, Def3;
hence x <=' y by A1, A28, Def5; :: thesis: verum
end;
end;