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 object holds not e in { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) }
proof
given e being object 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 object ; :: 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:79;
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
t0 <> {} by A10, ARYTM_3:64;
then A14: r1 *' t0 <> {} by A13, ARYTM_3:78;
A15: r = {} by A4, A11, ARYTM_3:48;
then r <=' r1 *' t0 by ARYTM_3:64;
hence r < r1 *' t0 by A15, A14, ARYTM_3:68; :: thesis: verum
end;
suppose A16: r0 <> {} ; :: thesis: ex s being Element of RAT+ st
( s in C & r < s )
s0 <> t0 by A10;
then A17: r <> r0 *' t0 by A4, A16, ARYTM_3:56;
take r0 *' t0 ; :: thesis: ( r0 *' t0 in C & r < r0 *' t0 )
thus r0 *' t0 in C by A5, A9; :: thesis: r < r0 *' t0
r <=' r0 *' t0 by A4, A10, ARYTM_3:82;
hence r < r0 *' t0 by A17, ARYTM_3:68; :: 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 :: thesis: not r0 *' s0 in C
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 & s1 in B ) ;
( r0 <=' r1 or s0 <=' s1 ) by A21, ARYTM_3:83;
hence contradiction by A19, A20, A22, 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:56; :: thesis: verum
end;
end;