{ (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } in DEDEKIND_CUTS

set C = { (s + t) where s, t is Element of RAT+ : ( s in A & t in B ) } ;
{ (s + t) where s, t is Element of RAT+ : ( s in A & t in B ) } c= RAT+

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in { (s + t) where s, t is Element of RAT+ : ( s in A & t in B ) } ; :: thesis:
then ex s, t being Element of RAT+ st
( e = s + t & s in A & t in B ) ;
hence e in RAT+ ; :: thesis:

end;

then reconsider C = { (s + t) where s, t is Element of RAT+ : ( s in A & t in B ) } as Subset of RAT+ ;
A <> RAT+ by ZFMISC_1:56;
then consider a0 being Element of RAT+ such that
A1: not a0 in A by SUBSET_1:28;
for r being Element of RAT+ st r in C holds
( ( for s being Element of RAT+ st s <=' r holds
s in C ) & ex s being Element of RAT+ st
( s in C & r < s ) )

let r be Element of RAT+ ; :: thesis:
assume r in C ; :: thesis:
then consider s0, t0 being Element of RAT+ such that
A2: r = s0 + t0 and
A3: s0 in A and
A4: t0 in B ;
thus for s being Element of RAT+ st s <=' r holds
s in C :: thesis:

let s be Element of RAT+ ; :: thesis:
assume s <=' r ; :: thesis:
then consider s1, t1 being Element of RAT+ such that
A5: s = s1 + t1 and
A6: ( s1 <=' s0 & t1 <=' t0 ) by A2, ARYTM_3:87;
( s1 in A & t1 in B ) by A3, A4, A6, Lm16;
hence s in C by A5; :: thesis:

end;

consider s1 being Element of RAT+ such that
A7: s1 in A and
A8: s0 < s1 by A3, Lm7;
take t2 = s1 + t0; :: thesis:
thus t2 in C by A4, A7; :: thesis:
thus r < t2 by A2, A8, ARYTM_3:76; :: thesis:

end;

then A9: C in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ;
B <> RAT+ by ZFMISC_1:56;
then consider b0 being Element of RAT+ such that
A10: not b0 in B by SUBSET_1:28;

assume a0 + b0 in C ; :: thesis:
then consider s, t being Element of RAT+ such that
A11: a0 + b0 = s + t and
A12: ( s in A & t in B ) ;
( a0 <=' s or b0 <=' t ) by A11, ARYTM_3:81;
hence contradiction by A1, A10, A12, Lm16; :: thesis:

end;

then C <> RAT+ ;
hence { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } in DEDEKIND_CUTS by A9, ZFMISC_1:56; :: thesis:

end;

hence { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS ; :: thesis: