{ (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+ ;
A <> RAT+ by ZFMISC_1:64;
then consider a0 being Element of RAT+ such that
A1: not a0 in A by SUBSET_1:49;
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
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: 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
A5: s = s1 + t1 and
A6: ( s1 <=' s0 & t1 <=' t0 ) by A2, ARYTM_3:95;
( s1 in A & t1 in B ) by A3, A4, A6, Lm16;
hence s in C by A5; :: thesis: verum

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: ( t2 in C & r < t2 )
thus t2 in C by A4, A7; :: thesis: r < t2
thus r < t2 by A2, A8, ARYTM_3:83; :: 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 ) ) } ;
B <> RAT+ by ZFMISC_1:64;
then consider b0 being Element of RAT+ such that
A10: 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
A11: a0 + b0 = s + t and
A12: ( s in A & t in B ) ;
( a0 <=' s or b0 <=' t ) by A11, ARYTM_3:89;
hence contradiction by A1, A10, 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