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
consider y' being Element of RAT+ such that
A4: y' in B and
A5: y' <> {} by A3, Lm15;
A <> RAT+ by ZFMISC_1:64;
then consider r being Element of RAT+ such that
A6: not r in A by SUBSET_1:49;
consider n being Element of RAT+ such that
A7: n in omega and
A8: r <=' n *' y' by A5, ARYTM_3:103;
defpred S₁[ Element of RAT+ ] means $1 *' y' in A;
A9: not S₁[n] by A6, A8, Lm16;
consider A0 being Element of RAT+ such that
A10: A0 in A by A2, SUBSET_1:10;
{} *' y' = {} by ARYTM_3:54;
then A11: S₁[ {} ] by A10, Lm16, ARYTM_3:71;
consider n0 being Element of RAT+ such that
n0 in omega and
A12: S₁[n0] and
A13: not S₁[n0 + one ] from ARYTM_3:sch 1(Lm32, Lm33, A7, A11, A9);
(n0 + one ) *' y' = (n0 *' y') + (one *' y') by ARYTM_3:63
.= (n0 *' y') + y' by ARYTM_3:59 ;
hence contradiction by A1, A4, A12, A13; :: thesis: verum