let A, B be Element of DEDEKIND_CUTS ; :: thesis: ( A + B = A & A <> {} implies B = {} )
assume that
A1: A + B = A and
A2: A <> {} and
A3: B <> {} ; :: thesis: contradiction
A4: ex A0 being Element of RAT+ st A0 in A by A2, SUBSET_1:4;
consider y9 being Element of RAT+ such that
A5: y9 in B and
A6: y9 <> {} by A3, Lm15;
defpred S₁[ Element of RAT+ ] means $1 *' y9 in A;
{} *' y9 = {} by ARYTM_3:48;
then A7: S₁[ {} ] by A4, Lm16, ARYTM_3:64;
A <> RAT+ by ZFMISC_1:56;
then consider r being Element of RAT+ such that
A8: not r in A by SUBSET_1:28;
consider n being Element of RAT+ such that
A9: n in omega and
A10: r <=' n *' y9 by A6, ARYTM_3:95;
A11: not S₁[n] by A8, A10, Lm16;
consider n0 being Element of RAT+ such that
n0 in omega and
A12: ( S₁[n0] & not S₁[n0 + one] ) from ARYTM_3:sch 1(Lm32, Lm33, A9, A7, A11);
(n0 + one) *' y9 = (n0 *' y9) + (one *' y9) by ARYTM_3:57
.= (n0 *' y9) + y9 by ARYTM_3:53 ;
hence contradiction by A1, A5, A12; :: thesis: verum