per cases ( A = {} or A <> {} ) ;

suppose A1: A = {} ; :: thesis: { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS

for e being set holds not e in { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) }

proof

given e being set such that A2: e in { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } ; :: thesis: contradiction
ex r, s being Element of RAT+ st
( e = r *' s & r in A & s in B ) by A2;
hence contradiction by A1; :: thesis: verum

end;

hence { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS by Lm8, XBOOLE_0:def 1; :: thesis: verum

end;

suppose A3: A <> {} ; :: thesis: { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS

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

proof

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

end;

then reconsider C = { (r *' s) where r, s is Element of RAT+ : ( r in A & s 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 r0, s0 being Element of RAT+ such that
A4: r = r0 *' s0 and
A5: r0 in A and
A6: s0 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 t0 being Element of RAT+ such that
A7: s = r0 *' t0 and
A8: t0 <=' s0 by A4, ARYTM_3:87;
t0 in B by A6, A8, Lm16;
hence s in C by A5, A7; :: thesis: verum

end;

consider t0 being Element of RAT+ such that
A9: t0 in B and
A10: s0 < t0 by A6, Lm7;

per cases ( r0 = {} or r0 <> {} ) ;

suppose A11: r0 = {} ; :: thesis: ex s being Element of RAT+ st
( s in C & r < s )

consider r1 being Element of RAT+ such that
A12: r1 in A and
A13: r1 <> {} by A3, Lm15;
take r1 *' t0 ; :: thesis: ( r1 *' t0 in C & r < r1 *' t0 )
thus r1 *' t0 in C by A9, A12; :: thesis: r < r1 *' t0
A14: r = {} by A4, A11, ARYTM_3:54;
then A15: r <=' r1 *' t0 by ARYTM_3:71;
t0 <> {} by A10, ARYTM_3:71;
then r1 *' t0 <> {} by A13, ARYTM_3:86;
hence r < r1 *' t0 by A14, A15, ARYTM_3:75; :: thesis: verum

end;

suppose A16: r0 <> {} ; :: thesis: ex s being Element of RAT+ st
( s in C & r < s )

take r0 *' t0 ; :: thesis: ( r0 *' t0 in C & r < r0 *' t0 )
thus r0 *' t0 in C by A5, A9; :: thesis: r < r0 *' t0
s0 <> t0 by A10;
then A17: r <> r0 *' t0 by A4, A16, ARYTM_3:62;
r <=' r0 *' t0 by A4, A10, ARYTM_3:90;
hence r < r0 *' t0 by A17, ARYTM_3:75; :: thesis: verum

end;

end;

end;

then A18: 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 ) ) } ;
consider r0 being Element of RAT+ such that
A19: not r0 in A by Lm24;
consider s0 being Element of RAT+ such that
A20: not s0 in B by Lm24;

now

assume r0 *' s0 in C ; :: thesis: contradiction
then consider r1, s1 being Element of RAT+ such that
A21: r0 *' s0 = r1 *' s1 and
A22: r1 in A and
A23: s1 in B ;
( r0 <=' r1 or s0 <=' s1 ) by A21, ARYTM_3:91;
hence contradiction by A19, A20, A22, A23, Lm16; :: thesis: verum

end;

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

end;

end;