let A be Element of DEDEKIND_CUTS ; :: thesis: ( A <> {} implies ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone )
assume A1: A <> {} ; :: thesis: ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone

per cases ( A in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } or not A in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ) ;

suppose A in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; :: thesis: ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone

then consider r0 being Element of RAT+ such that
A2: A = { s where s is Element of RAT+ : s < r0 } and
A3: r0 <> {} ;
consider s0 being Element of RAT+ such that
A4: r0 *' s0 = one by A3, ARYTM_3:60;
set B = { s where s is Element of RAT+ : s < s0 } ;
{ s where s is Element of RAT+ : s < s0 } c= RAT+

proof

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

end;

then reconsider B = { s where s is Element of RAT+ : s < s0 } as Subset of ;
for r being Element of RAT+ st r in B holds
( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ st
( s in B & r < s ) )

proof

let r be Element of RAT+ ; :: thesis: ( r in B implies ( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ st
( s in B & r < s ) ) )
assume r in B ; :: thesis: ( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ st
( s in B & r < s ) )
then A5: ex s being Element of RAT+ st
( s = r & s < s0 ) ;
then consider t being Element of RAT+ such that
A6: r < t and
A7: t < s0 by ARYTM_3:101;
thus for s being Element of RAT+ st s <=' r holds
s in B :: thesis: ex s being Element of RAT+ st
( s in B & r < s )

proof

let s be Element of RAT+ ; :: thesis: ( s <=' r implies s in B )
assume s <=' r ; :: thesis: s in B
then s < s0 by A5, ARYTM_3:76;
hence s in B ; :: thesis: verum

end;

take t ; :: thesis: ( t in B & r < t )
thus t in B by A7; :: thesis: r < t
thus r < t by A6; :: thesis: verum

end;

then A8: B in { A where A is Subset of : 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 ) ) } ;
for s being Element of RAT+ holds
( not s = s0 or not s < s0 ) ;
then not s0 in B ;
then B <> RAT+ ;
then reconsider B = B as Element of DEDEKIND_CUTS by A8, ZFMISC_1:64;
A9: A *' B = { s where s is Element of RAT+ : s < r0 *' s0 }

proof

thus A *' B c= { s where s is Element of RAT+ : s < r0 *' s0 } :: according to XBOOLE_0:def 10 :: thesis: { s where s is Element of RAT+ : s < r0 *' s0 } c= A *' B

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in A *' B or e in { s where s is Element of RAT+ : s < r0 *' s0 } )
assume e in A *' B ; :: thesis: e in { s where s is Element of RAT+ : s < r0 *' s0 }
then consider r1, s1 being Element of RAT+ such that
A10: e = r1 *' s1 and
A11: r1 in A and
A12: s1 in B ;
ex s being Element of RAT+ st
( s = r1 & s < r0 ) by A2, A11;
then A13: r1 *' s1 <=' r0 *' s1 by ARYTM_3:90;
A14: ex s being Element of RAT+ st
( s = s1 & s < s0 ) by A12;
then s1 <> s0 ;
then A15: r0 *' s1 <> r0 *' s0 by A3, ARYTM_3:62;
r0 *' s1 <=' r0 *' s0 by A14, ARYTM_3:90;
then r0 *' s1 < r0 *' s0 by A15, ARYTM_3:75;
then r1 *' s1 < r0 *' s0 by A13, ARYTM_3:76;
hence e in { s where s is Element of RAT+ : s < r0 *' s0 } by A10; :: thesis: verum

end;

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { s where s is Element of RAT+ : s < r0 *' s0 } or e in A *' B )
assume e in { s where s is Element of RAT+ : s < r0 *' s0 } ; :: thesis: e in A *' B
then consider s1 being Element of RAT+ such that
A16: e = s1 and
A17: s1 < r0 *' s0 ;
consider t0 being Element of RAT+ such that
A18: s1 = r0 *' t0 and
A19: t0 <=' s0 by A17, ARYTM_3:87;
t0 <> s0 by A17, A18;
then t0 < s0 by A19, ARYTM_3:75;
then t0 in B ;
then consider t1 being Element of RAT+ such that
A20: t1 in B and
A21: t0 < t1 by Lm7;
r0 *' t0 <=' t1 *' r0 by A21, ARYTM_3:90;
then consider r1 being Element of RAT+ such that
A22: r0 *' t0 = t1 *' r1 and
A23: r1 <=' r0 by ARYTM_3:87;
t0 <> t1 by A21;
then r1 <> r0 by A3, A22, ARYTM_3:62;
then r1 < r0 by A23, ARYTM_3:75;
then r1 in A by A2;
hence e in A *' B by A16, A18, A20, A22; :: thesis: verum

end;

ex t0 being Element of RAT+ st
( t0 = rone & DEDEKIND_CUT rone = { s where s is Element of RAT+ : s < t0 } ) by Def3;
hence ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone by A4, A9; :: thesis: verum

end;

suppose A24: not A in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; :: thesis: ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone

set B = { y' where y' is Element of RAT+ : ex x' being Element of RAT+ st
( not x' in A & x' *' y' <=' one ) } ;
A25: { y' where y' is Element of RAT+ : ex x' being Element of RAT+ st
( not x' in A & x' *' y' <=' one ) } c= RAT+

proof

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

end;

A26: A <> RAT+ by ZFMISC_1:64;
then consider x0 being Element of RAT+ such that
A27: not x0 in A by SUBSET_1:49;
x0 *' {} = {} by ARYTM_3:54;
then x0 *' {} <=' one by ARYTM_3:71;
then A28: {} in { y' where y' is Element of RAT+ : ex x' being Element of RAT+ st
( not x' in A & x' *' y' <=' one ) } by A27;
then reconsider B = { y' where y' is Element of RAT+ : ex x' being Element of RAT+ st
( not x' in A & x' *' y' <=' one ) } as non empty Subset of by A25;
A29: A in { A where A is Subset of : 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 ) ) } by ZFMISC_1:64;
ex x' being Element of RAT+ st x' in A by A1, SUBSET_1:10;
then A30: {} in A by A29, Lm29, ARYTM_3:71;
for r being Element of RAT+ st r in B holds
( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ st
( s in B & r < s ) )

proof

let r be Element of RAT+ ; :: thesis: ( r in B implies ( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ st
( s in B & r < s ) ) )
assume r in B ; :: thesis: ( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ st
( s in B & r < s ) )
then ex y' being Element of RAT+ st
( r = y' & ex x' being Element of RAT+ st
( not x' in A & x' *' y' <=' one ) ) ;
then consider x' being Element of RAT+ such that
A31: not x' in A and
A32: x' *' r <=' one ;
thus for s being Element of RAT+ st s <=' r holds
s in B :: thesis: ex s being Element of RAT+ st
( s in B & r < s )

proof

let s be Element of RAT+ ; :: thesis: ( s <=' r implies s in B )
assume s <=' r ; :: thesis: s in B
then x' *' s <=' x' *' r by ARYTM_3:90;
then x' *' s <=' one by A32, ARYTM_3:74;
hence s in B by A31; :: thesis: verum

end;

A in DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A24, XBOOLE_0:def 5;
then consider x'' being Element of RAT+ such that
A33: not x'' in A and
A34: x'' < x' by A1, A31, Lm18;
consider s being Element of RAT+ such that
A35: one = x'' *' s by A30, A33, ARYTM_3:61;
take s ; :: thesis: ( s in B & r < s )
x'' *' s <=' one by A35;
hence s in B by A33; :: thesis: r < s
A36: s <> {} by A35, ARYTM_3:54;
x'' *' r <=' x' *' r by A34, ARYTM_3:90;
then x'' *' r <=' x'' *' s by A32, A35, ARYTM_3:74;
then A37: r <=' s by A30, A33, ARYTM_3:88;
( x'' <> x' & x'' *' s <=' x' *' s ) by A34, ARYTM_3:90;
then r <> s by A32, A35, A36, ARYTM_3:62, ARYTM_3:73;
hence r < s by A37, ARYTM_3:75; :: thesis: verum

end;

then A38: B in { A where A is Subset of : 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 x' being Element of RAT+ such that
A39: x' in A and
A40: x' <> {} by A1, A29, Lm42;
consider y' being Element of RAT+ such that
A41: x' *' y' = one by A40, ARYTM_3:61;

now

assume y' in B ; :: thesis: contradiction
then A42: ex s being Element of RAT+ st
( s = y' & ex x' being Element of RAT+ st
( not x' in A & x' *' s <=' one ) ) ;
y' <> {} by A41, ARYTM_3:54;
hence contradiction by A29, A39, A41, A42, Lm29, ARYTM_3:88; :: thesis: verum

end;

then B <> RAT+ ;
then not B in {RAT+ } by TARSKI:def 1;
then reconsider B = B as Element of DEDEKIND_CUTS by A38, XBOOLE_0:def 5;
take B ; :: thesis: A *' B = DEDEKIND_CUT rone
for r being Element of RAT+ holds
( r in A *' B iff r < one )

proof

let r be Element of RAT+ ; :: thesis: ( r in A *' B iff r < one )

hereby :: thesis: ( r < one implies r in A *' B )

assume r in A *' B ; :: thesis: r < one
then consider s, t being Element of RAT+ such that
A43: r = s *' t and
A44: s in A and
A45: t in B ;
ex z' being Element of RAT+ st
( z' = t & ex x' being Element of RAT+ st
( not x' in A & x' *' z' <=' one ) ) by A45;
then consider x' being Element of RAT+ such that
A46: not x' in A and
A47: x' *' t <=' one ;
s <=' x' by A29, A44, A46, Lm29;
then A48: s *' t <=' x' *' t by ARYTM_3:90;

A49: now

assume A50: r = one ; :: thesis: contradiction
then t <> {} by A43, ARYTM_3:54;
hence contradiction by A43, A44, A46, A47, A48, A50, ARYTM_3:62, ARYTM_3:73; :: thesis: verum

end;

r <=' one by A43, A47, A48, ARYTM_3:74;
hence r < one by A49, ARYTM_3:75; :: thesis: verum

end;

assume A51: r < one ; :: thesis: r in A *' B
then A52: r <> one ;

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

suppose r = {} ; :: thesis: r in A *' B

then r = {} *' {} by ARYTM_3:54;
hence r in A *' B by A28, A30; :: thesis: verum

end;

suppose r <> {} ; :: thesis: r in A *' B

then consider r' being Element of RAT+ such that
A53: r *' r' = one by ARYTM_3:61;
{ (r *' s) where s is Element of RAT+ : s in A } c= RAT+

proof

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

end;

then reconsider rA = { (r *' s) where s is Element of RAT+ : s in A } as Subset of ;
consider dr being Element of RAT+ such that
A54: r + dr = one by A51, ARYTM_3:def 13;
consider xx being Element of RAT+ such that
A55: not xx in A by A26, SUBSET_1:49;
set rr = x' *' dr;
dr <> {} by A52, A54, ARYTM_3:56;
then consider n0 being Element of RAT+ such that
A56: n0 in omega and
A57: xx <=' n0 *' (x' *' dr) by A40, ARYTM_3:86, ARYTM_3:103;
defpred S₁[ Element of RAT+ ] means $1 *' (x' *' dr) in A;
A58: S₁[ {} ] by A30, ARYTM_3:54;
A59: not S₁[n0] by A29, A55, A57, Lm29;
consider n1 being Element of RAT+ such that
n1 in omega and
A60: S₁[n1] and
A61: not S₁[n1 + one ] from ARYTM_3:sch 1(Lm32, Lm33, A56, A58, A59);
set s0 = n1 *' (x' *' dr);

A62: now

assume n1 *' (x' *' dr) in rA ; :: thesis: contradiction
then consider s0 being Element of RAT+ such that
A63: r *' s0 = n1 *' (x' *' dr) and
A64: s0 in A ;
A65: (n1 + one ) *' (x' *' dr) = (n1 *' (x' *' dr)) + (one *' (x' *' dr)) by ARYTM_3:63
.= (r *' s0) + (dr *' x') by A63, ARYTM_3:59 ;
( s0 <=' x' or x' <=' s0 ) ;
then consider s1 being Element of RAT+ such that
A66: ( ( s1 = s0 & x' <=' s1 ) or ( s1 = x' & s0 <=' s1 ) ) ;
dr *' x' <=' dr *' s1 by A66, ARYTM_3:90;
then A67: (r *' s1) + (dr *' x') <=' (r *' s1) + (dr *' s1) by ARYTM_3:83;
r *' s0 <=' r *' s1 by A66, ARYTM_3:90;
then A68: (r *' s0) + (dr *' x') <=' (r *' s1) + (dr *' x') by ARYTM_3:83;
(r *' s1) + (dr *' s1) = (r + dr) *' s1 by ARYTM_3:63
.= s1 by A54, ARYTM_3:59 ;
hence contradiction by A29, A39, A61, A64, A65, A66, A68, A67, Lm29; :: thesis: verum

end;

A69: now

assume A70: (n1 *' (x' *' dr)) *' r' in A ; :: thesis: contradiction
r *' ((n1 *' (x' *' dr)) *' r') = one *' (n1 *' (x' *' dr)) by A53, ARYTM_3:58
.= n1 *' (x' *' dr) by ARYTM_3:59 ;
hence contradiction by A62, A70; :: thesis: verum

end;

r *' {} = {} by ARYTM_3:54;
then {} in rA by A30;
then consider s' being Element of RAT+ such that
A71: (n1 *' (x' *' dr)) *' s' = one by A62, ARYTM_3:61;
A72: (n1 *' (x' *' dr)) *' (r *' s') = ((n1 *' (x' *' dr)) *' s') *' r by ARYTM_3:58
.= r by A71, ARYTM_3:59 ;
((n1 *' (x' *' dr)) *' r') *' (r *' s') = (((n1 *' (x' *' dr)) *' r') *' r) *' s' by ARYTM_3:58
.= ((n1 *' (x' *' dr)) *' one ) *' s' by A53, ARYTM_3:58
.= one by A71, ARYTM_3:59 ;
then ((n1 *' (x' *' dr)) *' r') *' (r *' s') <=' one ;
then r *' s' in B by A69;
hence r in A *' B by A60, A72; :: thesis: verum

end;

end;

end;

then DEDEKIND_CUT (GLUED (A *' B)) = DEDEKIND_CUT rone by Def4;
hence A *' B = DEDEKIND_CUT rone by Lm12; :: thesis: verum

end;

end;