let A, B, C be Element of DEDEKIND_CUTS ; :: thesis: A + (B + C) c= (A + B) + C
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in A + (B + C) or e in (A + B) + C )
assume e in A + (B + C) ; :: thesis: e in (A + B) + C
then consider r0, s0 being Element of RAT+ such that
A1: ( e = r0 + s0 & r0 in A ) and
A2: s0 in B + C ;
consider r1, s1 being Element of RAT+ such that
A3: ( s0 = r1 + s1 & r1 in B ) and
A4: s1 in C by A2;
( e = (r0 + r1) + s1 & r0 + r1 in A + B ) by A1, A3, ARYTM_3:51;
hence e in (A + B) + C by A4; :: thesis: verum