let rone be Element of REAL+ ; :: thesis: ( rone = one implies for A being Element of DEDEKIND_CUTS st A <> {} holds
ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone )
assume A0: rone = one ; :: thesis: for A being Element of DEDEKIND_CUTS st A <> {} holds
ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone
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:54;
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 object ; :: 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 RAT+ ;
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:93;
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:69;
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 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 ) ) } ;
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:56;
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 object ; :: 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:82;
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:56;
r0 *' s1 <=' r0 *' s0 by A14, ARYTM_3:82;
then r0 *' s1 < r0 *' s0 by A15, ARYTM_3:68;
then r1 *' s1 < r0 *' s0 by A13, ARYTM_3:69;
hence e in { s where s is Element of RAT+ : s < r0 *' s0 } by A10; :: thesis: verum

end;

let e be object ; :: 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:79;
t0 <> s0 by A17, A18;
then t0 < s0 by A19, ARYTM_3:68;
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:82;
then consider r1 being Element of RAT+ such that
A22: r0 *' t0 = t1 *' r1 and
A23: r1 <=' r0 by ARYTM_3:79;
t0 <> t1 by A21;
then r1 <> r0 by A3, A22, ARYTM_3:56;
then r1 < r0 by A23, ARYTM_3:68;
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, A0;
hence ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone by A4, A9, A0; :: 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 = { y9 where y9 is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 *' y9 <=' one ) } ;
A25: { y9 where y9 is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 *' y9 <=' one ) } c= RAT+

proof

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

end;

A26: A <> RAT+ by ZFMISC_1:56;
then consider x0 being Element of RAT+ such that
A27: not x0 in A by SUBSET_1:28;
x0 *' {} = {} by ARYTM_3:48;
then x0 *' {} <=' one by ARYTM_3:64;
then A28: {} in { y9 where y9 is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 *' y9 <=' one ) } by A27;
then reconsider B = { y9 where y9 is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 *' y9 <=' one ) } as non empty Subset of RAT+ by A25;
A29: A 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 ) ) } by ZFMISC_1:56;
ex x9 being Element of RAT+ st x9 in A by A1, SUBSET_1:4;
then A30: {} in A by A29, Lm29, ARYTM_3:64;
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 y9 being Element of RAT+ st
( r = y9 & ex x9 being Element of RAT+ st
( not x9 in A & x9 *' y9 <=' one ) ) ;
then consider x9 being Element of RAT+ such that
A31: not x9 in A and
A32: x9 *' 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 x9 *' s <=' x9 *' r by ARYTM_3:82;
then x9 *' s <=' one by A32, ARYTM_3:67;
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 x99 being Element of RAT+ such that
A33: not x99 in A and
A34: x99 < x9 by A1, A31, Lm18;
consider s being Element of RAT+ such that
A35: one = x99 *' s by A30, A33, ARYTM_3:55;
take s ; :: thesis: ( s in B & r < s )
x99 *' s <=' one by A35;
hence s in B by A33; :: thesis: r < s
A36: s <> {} by A35, ARYTM_3:48;
x99 *' r <=' x9 *' r by A34, ARYTM_3:82;
then x99 *' r <=' x99 *' s by A32, A35, ARYTM_3:67;
then A37: r <=' s by A30, A33, ARYTM_3:80;
( x99 <> x9 & x99 *' s <=' x9 *' s ) by A34, ARYTM_3:82;
then r <> s by A32, A35, A36, ARYTM_3:56, ARYTM_3:66;
hence r < s by A37, ARYTM_3:68; :: thesis: verum

end;

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

now :: thesis: not y9 in B

assume y9 in B ; :: thesis: contradiction
then A42: ex s being Element of RAT+ st
( s = y9 & ex x9 being Element of RAT+ st
( not x9 in A & x9 *' s <=' one ) ) ;
y9 <> {} by A41, ARYTM_3:48;
hence contradiction by A29, A39, A41, A42, Lm29, ARYTM_3:80; :: 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 z9 being Element of RAT+ st
( z9 = t & ex x9 being Element of RAT+ st
( not x9 in A & x9 *' z9 <=' one ) ) by A45;
then consider x9 being Element of RAT+ such that
A46: not x9 in A and
A47: x9 *' t <=' one ;
s <=' x9 by A29, A44, A46, Lm29;
then A48: s *' t <=' x9 *' t by ARYTM_3:82;

A49: now :: thesis: not r = one

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

end;

r <=' one by A43, A47, A48, ARYTM_3:67;
hence r < one by A49, ARYTM_3:68; :: 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:48;
hence r in A *' B by A28, A30; :: thesis: verum

end;

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

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

proof

let e be object ; :: 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 RAT+ ;
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:28;
set rr = x9 *' dr;
dr <> {} by A52, A54, ARYTM_3:50;
then consider n0 being Element of RAT+ such that
A56: n0 in omega and
A57: xx <=' n0 *' (x9 *' dr) by A40, ARYTM_3:78, ARYTM_3:95;
defpred S₁[ Element of RAT+ ] means $1 *' (x9 *' dr) in A;
A58: S₁[ {} ] by A30, ARYTM_3:48;
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 *' (x9 *' dr);

A62: now :: thesis: not n1 *' (x9 *' dr) in rA

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

end;

A69: now :: thesis: not (n1 *' (x9 *' dr)) *' r9 in A

assume A70: (n1 *' (x9 *' dr)) *' r9 in A ; :: thesis: contradiction
r *' ((n1 *' (x9 *' dr)) *' r9) = one *' (n1 *' (x9 *' dr)) by A53, ARYTM_3:52
.= n1 *' (x9 *' dr) by ARYTM_3:53 ;
hence contradiction by A62, A70; :: thesis: verum

end;

r *' {} = {} by ARYTM_3:48;
then {} in rA by A30;
then consider s9 being Element of RAT+ such that
A71: (n1 *' (x9 *' dr)) *' s9 = one by A62, ARYTM_3:55;
A72: (n1 *' (x9 *' dr)) *' (r *' s9) = ((n1 *' (x9 *' dr)) *' s9) *' r by ARYTM_3:52
.= r by A71, ARYTM_3:53 ;
((n1 *' (x9 *' dr)) *' r9) *' (r *' s9) = (((n1 *' (x9 *' dr)) *' r9) *' r) *' s9 by ARYTM_3:52
.= ((n1 *' (x9 *' dr)) *' one) *' s9 by A53, ARYTM_3:52
.= one by A71, ARYTM_3:53 ;
then ((n1 *' (x9 *' dr)) *' r9) *' (r *' s9) <=' one ;
then r *' s9 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 A0, Def4;
hence A *' B = DEDEKIND_CUT rone by Lm12; :: thesis: verum

end;

end;