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

proof

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+

proof

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

end;

then reconsider C = { (s + t) where s, t is Element of RAT+ : ( s in A & t in B ) } as Subset of RAT+ ;
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 ) )

proof

let r be Element of RAT+ ; :: thesis: ( r in C implies ( ( 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 ) ) )
assume r in C ; :: thesis: ( ( 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 ) )
then consider s0, t0 being Element of RAT+ such that
A1: r = s0 + t0 and
A2: ( s0 in A & t0 in B ) ;
thus for s being Element of RAT+ st s <=' r holds
s in C :: thesis: ex s being Element of RAT+ st
( s in C & r < s )

proof

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

end;

consider s1 being Element of RAT+ such that
A7: s1 in A and
A8: s0 < s1 by A2, Lm7;
take t2 = s1 + t0; :: thesis: ( t2 in C & r < t2 )
thus t2 in C by A2, A7; :: thesis: r < t2
( s0 <=' s1 & s0 <> s1 ) by A8;
then ( r <=' t2 & r <> t2 ) by A1, ARYTM_3:69, ARYTM_3:83;
hence r < t2 by ARYTM_3:75; :: thesis: verum

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 ) ) } ;
A <> RAT+ by ZFMISC_1:64;
then consider a0 being Element of RAT+ such that
A10: not a0 in A by SUBSET_1:49;
B <> RAT+ by ZFMISC_1:64;
then consider b0 being Element of RAT+ such that
A11: not b0 in B by SUBSET_1:49;

now

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

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:64; :: thesis: verum

end;

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