:: ARYTM_2 semantic presentation

definition
func DEDEKIND_CUTS -> Subset-Family of RAT+ equals :: ARYTM_2:def 1
{ b1 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b2 in b1 implies ( ( for b2 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b2 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) } \ {RAT+ };
coherence
{ b1 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b2 in b1 implies ( ( for b2 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b2 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) } \ {RAT+ } is Subset-Family of RAT+
proof
set c1 = { b1 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b2 in b1 implies ( ( for b2 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b2 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) } ;
{ b1 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b2 in b1 implies ( ( for b2 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b2 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) } c= bool RAT+
proof
let c2 be set ; :: according to TARSKI:def 3
assume c2 in { b1 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b2 in b1 implies ( ( for b2 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b2 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) } ;
then ex b1 being Subset of RAT+ st
( c2 = b1 & ( for b2 being Element of RAT+ holds
( b2 in b1 implies ( ( for b3 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b3 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) ) ) ;
hence c2 in bool RAT+ ;
end;
hence { b1 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b2 in b1 implies ( ( for b2 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b2 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) } \ {RAT+ } is Subset-Family of RAT+ by XBOOLE_1:1;
end;
end;

:: deftheorem Def1 defines DEDEKIND_CUTS ARYTM_2:def 1 :
DEDEKIND_CUTS = { b1 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b2 in b1 implies ( ( for b2 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b2 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) } \ {RAT+ };

registration
cluster DEDEKIND_CUTS -> non empty ;
coherence
not DEDEKIND_CUTS is empty
proof
set c1 = { b1 where B is Element of RAT+ : b1 < one } ;
now
assume one in { b1 where B is Element of RAT+ : b1 < one } ;
then ex b1 being Element of RAT+ st
( b1 = one & b1 < one ) ;
hence not verum ;
end;
then E1: { b1 where B is Element of RAT+ : b1 < one } <> RAT+ ;
{} <=' one by ARYTM_3:71;
then {} < one by ARYTM_3:75;
then E2: {} in { b1 where B is Element of RAT+ : b1 < one } ;
{ b1 where B is Element of RAT+ : b1 < one } c= RAT+
proof
let c2 be set ; :: according to TARSKI:def 3
assume c2 in { b1 where B is Element of RAT+ : b1 < one } ;
then ex b1 being Element of RAT+ st
( b1 = c2 & b1 < one ) ;
hence c2 in RAT+ ;
end;
then reconsider c2 = { b1 where B is Element of RAT+ : b1 < one } as non empty Subset of RAT+ by E2;
for b1 being Element of RAT+ holds
( b1 in c2 implies ( ( for b2 being Element of RAT+ holds
( b2 <=' b1 implies b2 in c2 ) ) & ex b2 being Element of RAT+ st
( b2 in c2 & b1 < b2 ) ) )
proof
let c3 be Element of RAT+ ;
assume c3 in c2 ;
then E3: ex b1 being Element of RAT+ st
( b1 = c3 & b1 < one ) ;
thus for b1 being Element of RAT+ holds
( b1 <=' c3 implies b1 in c2 )
proof
let c4 be Element of RAT+ ;
assume c4 <=' c3 ;
then c4 < one by E3, ARYTM_3:74;
hence c4 in c2 ;
end;
consider c4 being Element of RAT+ such that
E4: c3 < c4 and
E5: c4 < one by E3, ARYTM_3:101;
take c4 ;
thus c4 in c2 by E5;
thus c3 < c4 by E4;
end;
then c2 in { b1 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b2 in b1 implies ( ( for b2 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b2 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) } ;
hence not DEDEKIND_CUTS is empty by E1, ZFMISC_1:64;
end;
end;

definition
func REAL+ -> set equals :: ARYTM_2:def 2
(RAT+ \/ DEDEKIND_CUTS ) \ { { b2 where B is Element of RAT+ : b2 < b1 } where B is Element of RAT+ : b1 <> {} } ;
coherence
(RAT+ \/ DEDEKIND_CUTS ) \ { { b2 where B is Element of RAT+ : b2 < b1 } where B is Element of RAT+ : b1 <> {} } is set ;
end;

:: deftheorem Def2 defines REAL+ ARYTM_2:def 2 :
REAL+ = (RAT+ \/ DEDEKIND_CUTS ) \ { { b2 where B is Element of RAT+ : b2 < b1 } where B is Element of RAT+ : b1 <> {} } ;

set c1 = { b1 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b2 in b1 implies ( ( for b2 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b2 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) } ;

set c2 = { { b2 where B is Element of RAT+ : b2 < b1 } where B is Element of RAT+ : b1 <> {} } ;

Lemma1: for b1, b2 being set holds
not [b1,b2] in { b3 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b4 in b3 implies ( ( for b2 being Element of RAT+ holds
( b5 <=' b4 implies b5 in b3 ) ) & ex b2 being Element of RAT+ st
( b5 in b3 & b4 < b5 ) ) ) }
proof
given c3, c4 being set such that E2: [c3,c4] in { b1 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b2 in b1 implies ( ( for b2 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b2 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) } ;
consider c5 being Subset of RAT+ such that
E3: [c3,c4] = c5 and
E4: for b1 being Element of RAT+ holds
( b1 in c5 implies ( ( for b2 being Element of RAT+ holds
( b2 <=' b1 implies b2 in c5 ) ) & ex b2 being Element of RAT+ st
( b2 in c5 & b1 < b2 ) ) ) by E2;
c5 = {{c3},{c3,c4}} by E3;
then E5: {c3} in c5 by TARSKI:def 2;
for b1, b2 being Element of RAT+ holds
( b1 in c5 & b2 <=' b1 implies b2 in c5 ) by E4;
then consider c6, c7, c8 being Element of RAT+ such that
E6: ( c6 in c5 & c7 in c5 & c8 in c5 ) and
E7: ( c6 <> c7 & c7 <> c8 & c8 <> c6 ) by E5, ARYTM_3:82;
( ( c6 = {c3,c4} or c6 = {c3} ) & ( c7 = {c3,c4} or c7 = {c3} ) & ( c8 = {c3,c4} or c8 = {c3} ) ) by E3, E6, TARSKI:def 2;
hence not verum by E7;
end;

Lemma2: RAT+ c= RAT+ \/ DEDEKIND_CUTS
by XBOOLE_1:7;

Lemma3: RAT+ misses { { b2 where B is Element of RAT+ : b2 < b1 } where B is Element of RAT+ : b1 <> {} }
proof
assume RAT+ meets { { b2 where B is Element of RAT+ : b2 < b1 } where B is Element of RAT+ : b1 <> {} } ;
then consider c3 being set such that
E4: c3 in RAT+ and
E5: c3 in { { b2 where B is Element of RAT+ : b2 < b1 } where B is Element of RAT+ : b1 <> {} } by XBOOLE_0:3;
consider c4 being Element of RAT+ such that
E6: c3 = { b1 where B is Element of RAT+ : b1 < c4 } and
E7: c4 <> {} by E5;
{} <=' c4 by ARYTM_3:71;
then {} < c4 by E7, ARYTM_3:75;
then E8: {} in c3 by E6;
c3 c= RAT+
proof
let c5 be set ; :: according to TARSKI:def 3
assume c5 in c3 ;
then ex b1 being Element of RAT+ st
( b1 = c5 & b1 < c4 ) by E6;
hence c5 in RAT+ ;
end;
then reconsider c5 = c3 as non empty Subset of RAT+ by E8;
consider c6 being Element of RAT+ such that
E9: c6 in c5 and
E10: for b1 being Element of RAT+ holds
( b1 in c5 implies b1 <=' c6 ) by E4, ARYTM_3:99;
ex b1 being Element of RAT+ st
( b1 = c6 & b1 < c4 ) by E6, E9;
then consider c7 being Element of RAT+ such that
E11: c6 < c7 and
E12: c7 < c4 by ARYTM_3:101;
c7 in c5 by E6, E12;
hence not verum by E10, E11;
end;

theorem Th1: :: ARYTM_2:1
RAT+ c= REAL+ by Lemma2, Lemma3, XBOOLE_1:86;

RAT+ \/ DEDEKIND_CUTS c= RAT+ \/ { b1 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b2 in b1 implies ( ( for b2 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b2 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) }
by XBOOLE_1:9;

then Lemma5: REAL+ c= RAT+ \/ { b1 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b2 in b1 implies ( ( for b2 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b2 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) }
by XBOOLE_1:1;

REAL+ = RAT+ \/ (({ b1 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b2 in b1 implies ( ( for b2 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b2 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) } \ {RAT+ }) \ { { b2 where B is Element of RAT+ : b2 < b1 } where B is Element of RAT+ : b1 <> {} } )
by Lemma3, XBOOLE_1:87;

then Lemma6: DEDEKIND_CUTS \ { { b2 where B is Element of RAT+ : b2 < b1 } where B is Element of RAT+ : b1 <> {} } c= REAL+
by XBOOLE_1:7;

theorem Th2: :: ARYTM_2:2
omega c= REAL+ by Th1, ARYTM_3:34, XBOOLE_1:1;

registration
cluster REAL+ -> non empty ;
coherence
not REAL+ is empty by Th2, ORDINAL2:19;
end;

definition
let c3 be Element of REAL+ ;
func DEDEKIND_CUT c1 -> Element of DEDEKIND_CUTS means :Def3: :: ARYTM_2:def 3
ex b1 being Element of RAT+ st
( a1 = b1 & a2 = { b2 where B is Element of RAT+ : b2 < b1 } ) if a1 in RAT+
otherwise a2 = a1;
existence
( not ( c3 in RAT+ & ( for b1 being Element of DEDEKIND_CUTS
for b2 being Element of RAT+ holds
not ( c3 = b2 & b1 = { b3 where B is Element of RAT+ : b3 < b2 } ) ) ) & not ( not c3 in RAT+ & ( for b1 being Element of DEDEKIND_CUTS holds
not b1 = c3 ) ) )
proof
thus not ( c3 in RAT+ & ( for b1 being Element of DEDEKIND_CUTS
for b2 being Element of RAT+ holds
not ( c3 = b2 & b1 = { b3 where B is Element of RAT+ : b3 < b2 } ) ) )
proof
assume c3 in RAT+ ;
then reconsider c4 = c3 as Element of RAT+ ;
set c5 = { b1 where B is Element of RAT+ : b1 < c4 } ;
for b1 being Element of RAT+ holds
not ( b1 = c4 & b1 < c4 ) ;
then not c4 in { b1 where B is Element of RAT+ : b1 < c4 } ;
then E8: { b1 where B is Element of RAT+ : b1 < c4 } <> RAT+ ;
{ b1 where B is Element of RAT+ : b1 < c4 } c= RAT+
proof
let c6 be set ; :: according to TARSKI:def 3
assume c6 in { b1 where B is Element of RAT+ : b1 < c4 } ;
then ex b1 being Element of RAT+ st
( b1 = c6 & b1 < c4 ) ;
hence c6 in RAT+ ;
end;
then reconsider c6 = { b1 where B is Element of RAT+ : b1 < c4 } as Subset of RAT+ ;
for b1 being Element of RAT+ holds
( b1 in c6 implies ( ( for b2 being Element of RAT+ holds
( b2 <=' b1 implies b2 in c6 ) ) & ex b2 being Element of RAT+ st
( b2 in c6 & b1 < b2 ) ) )
proof
let c7 be Element of RAT+ ;
assume c7 in c6 ;
then E9: ex b1 being Element of RAT+ st
( c7 = b1 & b1 < c4 ) ;
thus for b1 being Element of RAT+ holds
( b1 <=' c7 implies b1 in c6 )
proof
let c8 be Element of RAT+ ;
assume c8 <=' c7 ;
then c8 < c4 by E9, ARYTM_3:76;
hence c8 in c6 ;
end;
consider c8 being Element of RAT+ such that
E10: c7 < c8 and
E11: c8 < c4 by E9, ARYTM_3:101;
take c8 ;
thus c8 in c6 by E11;
thus c7 < c8 by E10;
end;
then c6 in { b1 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b2 in b1 implies ( ( for b2 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b2 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) } ;
then reconsider c7 = c6 as Element of DEDEKIND_CUTS by E8, ZFMISC_1:64;
take c7 ;
take c4 ;
thus ( c3 = c4 & c7 = { b1 where B is Element of RAT+ : b1 < c4 } ) ;
end;
assume E8: not c3 in RAT+ ;
c3 in REAL+ ;
then c3 in DEDEKIND_CUTS by E8, XBOOLE_0:def 2;
hence ex b1 being Element of DEDEKIND_CUTS st b1 = c3 ;
end;
uniqueness
for b1, b2 being Element of DEDEKIND_CUTS holds
( ( c3 in RAT+ & ex b3 being Element of RAT+ st
( c3 = b3 & b1 = { b4 where B is Element of RAT+ : b4 < b3 } ) & ex b3 being Element of RAT+ st
( c3 = b3 & b2 = { b4 where B is Element of RAT+ : b4 < b3 } ) implies b1 = b2 ) & ( not c3 in RAT+ & b1 = c3 & b2 = c3 implies b1 = b2 ) ) ;
consistency
for b1 being Element of DEDEKIND_CUTS holds
verum ;
end;

:: deftheorem Def3 defines DEDEKIND_CUT ARYTM_2:def 3 :
for b1 being Element of REAL+
for b2 being Element of DEDEKIND_CUTS holds
( ( b1 in RAT+ implies ( b2 = DEDEKIND_CUT b1 iff ex b3 being Element of RAT+ st
( b1 = b3 & b2 = { b4 where B is Element of RAT+ : b4 < b3 } ) ) ) & ( not b1 in RAT+ implies ( b2 = DEDEKIND_CUT b1 iff b2 = b1 ) ) );

theorem Th3: :: ARYTM_2:3
for b1 being set holds
not [{} ,b1] in REAL+
proof
given c3 being set such that E9: [{} ,c3] in REAL+ ;
per cases ( [{} ,c3] in RAT+ or [{} ,c3] in { b1 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b2 in b1 implies ( ( for b2 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b2 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) } ) by E9, Lemma5, XBOOLE_0:def 2;
suppose [{} ,c3] in RAT+ ;
hence not verum by ARYTM_3:68;
end;
suppose [{} ,c3] in { b1 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b2 in b1 implies ( ( for b2 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b2 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) } ;
hence not verum by Lemma1;
end;
end;
end;

Lemma9: for b1, b2 being Element of RAT+ holds
( ( for b3 being Element of RAT+ holds
( not ( b3 < b1 & not b3 < b2 ) & not ( b3 < b2 & not b3 < b1 ) ) ) implies b1 = b2 )
proof
let c3, c4 be Element of RAT+ ;
assume E10: for b1 being Element of RAT+ holds
( not ( b1 < c3 & not b1 < c4 ) & not ( b1 < c4 & not b1 < c3 ) ) ;
( c3 <=' c3 & c4 <=' c4 ) ;
then ( c3 <=' c4 & c4 <=' c3 ) by E10;
hence c3 = c4 by ARYTM_3:73;
end;

definition
let c3 be Element of DEDEKIND_CUTS ;
func GLUED c1 -> Element of REAL+ means :Def4: :: ARYTM_2:def 4
ex b1 being Element of RAT+ st
( a2 = b1 & ( for b2 being Element of RAT+ holds
( b2 in a1 iff b2 < b1 ) ) ) if ex b1 being Element of RAT+ st
for b2 being Element of RAT+ holds
( b2 in a1 iff b2 < b1 )
otherwise a2 = a1;
uniqueness
for b1, b2 being Element of REAL+ holds
( ( ex b3 being Element of RAT+ st
for b4 being Element of RAT+ holds
( b4 in c3 iff b4 < b3 ) & ex b3 being Element of RAT+ st
( b1 = b3 & ( for b4 being Element of RAT+ holds
( b4 in c3 iff b4 < b3 ) ) ) & ex b3 being Element of RAT+ st
( b2 = b3 & ( for b4 being Element of RAT+ holds
( b4 in c3 iff b4 < b3 ) ) ) implies b1 = b2 ) & ( ( for b3 being Element of RAT+ holds
not for b4 being Element of RAT+ holds
( b4 in c3 iff b4 < b3 ) ) & b1 = c3 & b2 = c3 implies b1 = b2 ) )
proof
let c4, c5 be Element of REAL+ ;
hereby
assume ex b1 being Element of RAT+ st
for b2 being Element of RAT+ holds
( b2 in c3 iff b2 < b1 ) ;
given c6 being Element of RAT+ such that E10: c4 = c6 and
E11: for b1 being Element of RAT+ holds
( b1 in c3 iff b1 < c6 ) ;
given c7 being Element of RAT+ such that E12: c5 = c7 and
E13: for b1 being Element of RAT+ holds
( b1 in c3 iff b1 < c7 ) ;
for b1 being Element of RAT+ holds
( not ( b1 < c6 & not b1 < c7 ) & not ( b1 < c7 & not b1 < c6 ) )
proof
let c8 be Element of RAT+ ;
( c8 in c3 iff c8 < c6 ) by E11;
hence ( not ( c8 < c6 & not c8 < c7 ) & not ( c8 < c7 & not c8 < c6 ) ) by E13;
end;
hence c4 = c5 by E10, E12, Lemma9;
end;
thus ( ( for b1 being Element of RAT+ holds
not for b2 being Element of RAT+ holds
( b2 in c3 iff b2 < b1 ) ) & c4 = c3 & c5 = c3 implies c4 = c5 ) ;
end;
existence
( not ( ex b1 being Element of RAT+ st
for b2 being Element of RAT+ holds
( b2 in c3 iff b2 < b1 ) & ( for b1 being Element of REAL+
for b2 being Element of RAT+ holds
not ( b1 = b2 & ( for b3 being Element of RAT+ holds
( b3 in c3 iff b3 < b2 ) ) ) ) ) & not ( ( for b1 being Element of RAT+ holds
not for b2 being Element of RAT+ holds
( b2 in c3 iff b2 < b1 ) ) & ( for b1 being Element of REAL+ holds
not b1 = c3 ) ) )
proof
hereby
given c4 being Element of RAT+ such that E10: for b1 being Element of RAT+ holds
( b1 in c3 iff b1 < c4 ) ;
c4 in RAT+ ;
then reconsider c5 = c4 as Element of REAL+ by Th1;
take c6 = c5;
take c7 = c4;
thus c6 = c7 ;
thus for b1 being Element of RAT+ holds
( b1 in c3 iff b1 < c7 ) by E10;
end;
assume E10: for b1 being Element of RAT+ holds
not for b2 being Element of RAT+ holds
( b2 in c3 iff b2 < b1 ) ;
now
assume c3 in { { b2 where B is Element of RAT+ : b2 < b1 } where B is Element of RAT+ : b1 <> {} } ;
then consider c4 being Element of RAT+ such that
E11: c3 = { b1 where B is Element of RAT+ : b1 < c4 } and
c4 <> {} ;
for b1 being Element of RAT+ holds
( b1 in c3 iff b1 < c4 )
proof
let c5 be Element of RAT+ ;
hereby
assume c5 in c3 ;
then ex b1 being Element of RAT+ st
( c5 = b1 & b1 < c4 ) by E11;
hence c5 < c4 ;
end;
thus ( c5 < c4 implies c5 in c3 ) by E11;
end;
hence not verum by E10;
end;
then c3 in DEDEKIND_CUTS \ { { b2 where B is Element of RAT+ : b2 < b1 } where B is Element of RAT+ : b1 <> {} } by XBOOLE_0:def 4;
then reconsider c4 = c3 as Element of REAL+ by Lemma6;
take c4 ;
thus c4 = c3 ;
end;
consistency
for b1 being Element of REAL+ holds
verum ;
end;

:: deftheorem Def4 defines GLUED ARYTM_2:def 4 :
for b1 being Element of DEDEKIND_CUTS
for b2 being Element of REAL+ holds
( ( ex b3 being Element of RAT+ st
for b4 being Element of RAT+ holds
( b4 in b1 iff b4 < b3 ) implies ( b2 = GLUED b1 iff ex b3 being Element of RAT+ st
( b2 = b3 & ( for b4 being Element of RAT+ holds
( b4 in b1 iff b4 < b3 ) ) ) ) ) & ( ( for b3 being Element of RAT+ holds
not for b4 being Element of RAT+ holds
( b4 in b1 iff b4 < b3 ) ) implies ( b2 = GLUED b1 iff b2 = b1 ) ) );

Lemma11: for b1 being Element of RAT+
for b2 being set holds
not ( b2 in DEDEKIND_CUTS & b1 in b2 & ( for b3 being Element of RAT+ holds
not ( b3 in b2 & b1 < b3 ) ) )
proof
let c3 be Element of RAT+ ;
let c4 be set ;
assume c4 in DEDEKIND_CUTS ;
then c4 in { b1 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b2 in b1 implies ( ( for b2 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b2 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) } ;
then ex b1 being Subset of RAT+ st
( c4 = b1 & ( for b2 being Element of RAT+ holds
( b2 in b1 implies ( ( for b3 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b3 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) ) ) ;
hence not ( c3 in c4 & ( for b1 being Element of RAT+ holds
not ( b1 in c4 & c3 < b1 ) ) ) ;
end;

Lemma12: {} in DEDEKIND_CUTS
proof
reconsider c3 = {} as Subset of RAT+ by XBOOLE_1:2;
for b1 being Element of RAT+ holds
( b1 in c3 implies ( ( for b2 being Element of RAT+ holds
( b2 <=' b1 implies b2 in c3 ) ) & ex b2 being Element of RAT+ st
( b2 in c3 & b1 < b2 ) ) ) ;
then {} in { b1 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b2 in b1 implies ( ( for b2 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b2 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) } ;
hence {} in DEDEKIND_CUTS by ZFMISC_1:64;
end;

Lemma13: DEDEKIND_CUTS /\ RAT+ = {{} }
proof
now
let c3 be set ;
thus ( c3 in DEDEKIND_CUTS /\ RAT+ implies c3 = {} )
proof
assume that
E14: c3 in DEDEKIND_CUTS /\ RAT+ and
E15: c3 <> {} ;
E16: c3 in DEDEKIND_CUTS by E14, XBOOLE_0:def 3;
then reconsider c4 = c3 as non empty Subset of RAT+ by E15;
c4 in RAT+ by E14, XBOOLE_0:def 3;
then ex b1 being Element of RAT+ st
( b1 in c4 & ( for b2 being Element of RAT+ holds
( b2 in c4 implies b2 <=' b1 ) ) ) by ARYTM_3:99;
hence not verum by E16, Lemma11;
end;
thus ( c3 = {} implies c3 in DEDEKIND_CUTS /\ RAT+ ) by Lemma12, XBOOLE_0:def 3;
end;
hence DEDEKIND_CUTS /\ RAT+ = {{} } by TARSKI:def 1;
end;

Lemma14: for b1 being Element of REAL+ holds
( DEDEKIND_CUT b1 = {} iff b1 = {} )
proof
let c3 be Element of REAL+ ;
thus ( DEDEKIND_CUT c3 = {} implies c3 = {} )
proof
assume E15: DEDEKIND_CUT c3 = {} ;
per cases not ( not c3 in RAT+ & c3 in RAT+ ) ;
suppose c3 in RAT+ ;
then consider c4 being Element of RAT+ such that
E16: c3 = c4 and
E17: DEDEKIND_CUT c3 = { b1 where B is Element of RAT+ : b1 < c4 } by Def3;
assume E18: c3 <> {} ;
{} <=' c4 by ARYTM_3:71;
then {} < c4 by E16, E18, ARYTM_3:75;
then {} in DEDEKIND_CUT c3 by E17;
hence not verum by E15;
end;
suppose not c3 in RAT+ ;
hence c3 = {} by E15, Def3;
end;
end;
end;
E15: for b1 being set holds
not b1 in { b2 where B is Element of RAT+ : b2 < {} }
proof
given c4 being set such that E16: c4 in { b1 where B is Element of RAT+ : b1 < {} } ;
ex b1 being Element of RAT+ st
( b1 = c4 & b1 < {} ) by E16;
hence not verum by ARYTM_3:71;
end;
assume c3 = {} ;
then ex b1 being Element of RAT+ st
( {} = b1 & DEDEKIND_CUT c3 = { b2 where B is Element of RAT+ : b2 < b1 } ) by Def3;
hence DEDEKIND_CUT c3 = {} by E15, XBOOLE_0:def 1;
end;

Lemma15: for b1 being Element of DEDEKIND_CUTS holds
( GLUED b1 = {} iff b1 = {} )
proof
let c3 be Element of DEDEKIND_CUTS ;
thus ( GLUED c3 = {} implies c3 = {} )
proof
assume E16: GLUED c3 = {} ;
per cases not ( ( for b1 being Element of RAT+ holds
not for b2 being Element of RAT+ holds
( b2 in c3 iff b2 < b1 ) ) & ex b1 being Element of RAT+ st
for b2 being Element of RAT+ holds
( b2 in c3 iff b2 < b1 ) ) ;
suppose ex b1 being Element of RAT+ st
for b2 being Element of RAT+ holds
( b2 in c3 iff b2 < b1 ) ;
then E17: ex b1 being Element of RAT+ st
( GLUED c3 = b1 & ( for b2 being Element of RAT+ holds
( b2 in c3 iff b2 < b1 ) ) ) by Def4;
assume c3 <> {} ;
then consider c4 being Element of RAT+ such that
E18: c4 in c3 by SUBSET_1:10;
c4 < {} by E16, E17, E18;
hence not verum by ARYTM_3:71;
end;
suppose for b1 being Element of RAT+ holds
not for b2 being Element of RAT+ holds
( b2 in c3 iff b2 < b1 ) ;
hence c3 = {} by E16, Def4;
end;
end;
end;
assume E16: c3 = {} ;
then for b1 being Element of RAT+ holds
( b1 in c3 iff b1 < {} ) by ARYTM_3:71;
then consider c4 being Element of RAT+ such that
E17: GLUED c3 = c4 and
E18: for b1 being Element of RAT+ holds
( b1 in c3 iff b1 < c4 ) by Def4;
assume E19: GLUED c3 <> {} ;
{} <=' c4 by ARYTM_3:71;
then {} < c4 by E17, E19, ARYTM_3:75;
hence not verum by E16, E18;
end;

Lemma16: for b1 being Element of DEDEKIND_CUTS holds DEDEKIND_CUT (GLUED b1) = b1
proof
let c3 be Element of DEDEKIND_CUTS ;
per cases not ( ( for b1 being Element of RAT+ holds
not for b2 being Element of RAT+ holds
( b2 in c3 iff b2 < b1 ) ) & not c3 = {} & not ( c3 <> {} & ( for b1 being Element of RAT+ holds
not for b2 being Element of RAT+ holds
( b2 in c3 iff b2 < b1 ) ) ) ) ;
suppose ex b1 being Element of RAT+ st
for b2 being Element of RAT+ holds
( b2 in c3 iff b2 < b1 ) ;
then consider c4 being Element of RAT+ such that
E17: c4 = GLUED c3 and
E18: for b1 being Element of RAT+ holds
( b1 in c3 iff b1 < c4 ) by Def4;
consider c5 being Element of RAT+ such that
E19: c4 = c5 and
E20: DEDEKIND_CUT (GLUED c3) = { b1 where B is Element of RAT+ : b1 < c5 } by E17, Def3;
thus DEDEKIND_CUT (GLUED c3) c= c3 :: according to XBOOLE_0:def 10
proof
let c6 be set ; :: according to TARSKI:def 3
assume c6 in DEDEKIND_CUT (GLUED c3) ;
then ex b1 being Element of RAT+ st
( b1 = c6 & b1 < c5 ) by E20;
hence c6 in c3 by E18, E19;
end;
let c6 be set ; :: according to TARSKI:def 3
assume E21: c6 in c3 ;
then reconsider c7 = c6 as Element of RAT+ ;
c7 < c4 by E18, E21;
hence c6 in DEDEKIND_CUT (GLUED c3) by E19, E20;
end;
suppose E17: c3 = {} ;
then GLUED c3 = {} by Lemma15;
hence DEDEKIND_CUT (GLUED c3) = c3 by E17, Lemma14;
end;
suppose that E17: c3 <> {} and
E18: for b1 being Element of RAT+ holds
not for b2 being Element of RAT+ holds
( b2 in c3 iff b2 < b1 ) ;
E19: GLUED c3 = c3 by E18, Def4;
now
assume GLUED c3 in RAT+ ;
then GLUED c3 in RAT+ /\ DEDEKIND_CUTS by E19, XBOOLE_0:def 3;
then GLUED c3 = {} by Lemma13, TARSKI:def 1;
hence not verum by E17, Lemma15;
end;
hence DEDEKIND_CUT (GLUED c3) = c3 by E19, Def3;
end;
end;
end;

Lemma17: for b1, b2 being set holds
not ( b1 in { b3 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b4 in b3 implies ( ( for b2 being Element of RAT+ holds
( b5 <=' b4 implies b5 in b3 ) ) & ex b2 being Element of RAT+ st
( b5 in b3 & b4 < b5 ) ) ) } & b2 in { b3 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b4 in b3 implies ( ( for b2 being Element of RAT+ holds
( b5 <=' b4 implies b5 in b3 ) ) & ex b2 being Element of RAT+ st
( b5 in b3 & b4 < b5 ) ) ) } & not b1 c= b2 & not b2 c= b1 )
proof
let c3, c4 be set ;
assume c3 in { b1 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b2 in b1 implies ( ( for b2 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b2 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) } ;
then consider c5 being Subset of RAT+ such that
E18: c3 = c5 and
E19: for b1 being Element of RAT+ holds
( b1 in c5 implies ( ( for b2 being Element of RAT+ holds
( b2 <=' b1 implies b2 in c5 ) ) & ex b2 being Element of RAT+ st
( b2 in c5 & b1 < b2 ) ) ) ;
assume c4 in { b1 where B is Subset of RAT+ : for b1 being Element of RAT+ holds
( b2 in b1 implies ( ( for b2 being Element of RAT+ holds
( b3 <=' b2 implies b3 in b1 ) ) & ex b2 being Element of RAT+ st
( b3 in b1 & b2 < b3 ) ) ) } ;
then consider c6 being Subset of RAT+ such that
E20: c4 = c6 and
E21: for b1 being Element of RAT+ holds
( b1 in c6 implies ( ( for b2 being Element of RAT+ holds
( b2 <=' b1 implies b2 in c6 ) ) & ex b2 being Element of RAT+ st
( b2 in c6 & b1 < b2 ) ) ) ;
assume not c3 c= c4 ;
then consider c7 being set such that
E22: c7 in c3 and
E23: not c7 in c4 by TARSKI:def 3;
reconsider c8 = c7 as Element of RAT+ by E18, E22;
let c9 be set ; :: according to TARSKI:def 3
assume E24: c9 in c4 ;