:: 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 ) ) ) } ;
E1: { 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+ } c= { 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:36;
{ 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 E1, XBOOLE_1:1;
end;
end;

:: deftheorem 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 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 <> {} } ;

E1: 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;

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

E3: 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 E4: :: ARYTM_2:1
RAT+ c= REAL+ by E2, E3, XBOOLE_1:86;

E5: REAL+ c= RAT+ \/ DEDEKIND_CUTS
by XBOOLE_1:36;

DEDEKIND_CUTS c= { 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:36;

then 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 E6: 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 E5, 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 E3, XBOOLE_1:87;

then E7: 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 E8: :: ARYTM_2:2
omega c= REAL+ by E4, ARYTM_3:34, XBOOLE_1:1;

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

definition
let c3 be Element of REAL+ ;
func DEDEKIND_CUT c1 -> Element of DEDEKIND_CUTS means :E9: :: 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 E9: { 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 E10: 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 E10, ARYTM_3:76;
hence c8 in c6 ;
end;
consider c8 being Element of RAT+ such that
E11: c7 < c8 and
E12: c8 < c4 by E10, ARYTM_3:101;
take c8 ;
thus c8 in c6 by E12;
thus c7 < c8 by E11;
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 E9, ZFMISC_1:64;
take c7 ;
take c4 ;
thus ( c3 = c4 & c7 = { b1 where B is Element of RAT+ : b1 < c4 } ) ;
end;
assume E9: not c3 in RAT+ ;
c3 in REAL+ ;
then c3 in DEDEKIND_CUTS by E9, E5, 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+ ) implies ( ( for b3 being Element of RAT+ holds
not ( c3 = b3 & b1 = { b4 where B is Element of RAT+ : b4 < b3 } ) ) or ( for b3 being Element of RAT+ holds
not ( c3 = b3 & b2 = { b4 where B is Element of RAT+ : b4 < b3 } ) ) or b1 = b2 ) ) & ( ( b1 = c3 & b2 = c3 ) implies ( c3 in RAT+ or b1 = b2 ) ) ) ;
consistency
for b1 being Element of DEDEKIND_CUTS holds
verum ;
end;

:: deftheorem E9 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 :: ARYTM_2:3
for b1 being set holds
not [{} ,b1] in REAL+
proof
given c3 being set such that E10: [{} ,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 E10, E6, 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 E1;
end;
end;
end;

E10: 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 E11: 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 E11;
hence c3 = c4 by ARYTM_3:73;
end;

definition
let c3 be Element of DEDEKIND_CUTS ;
func GLUED c1 -> Element of REAL+ means :E11: :: 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
( ( ( ) implies ( ( for b3 being Element of RAT+ holds
not for b4 being Element of RAT+ holds
( b4 in c3 iff b4 < b3 ) ) or ( for b3 being Element of RAT+ holds
not ( b1 = b3 & ( for b4 being Element of RAT+ holds
( b4 in c3 iff b4 < b3 ) ) ) ) or ( for b3 being Element of RAT+ holds
not ( b2 = b3 & ( for b4 being Element of RAT+ holds
( b4 in c3 iff b4 < b3 ) ) ) ) or 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 E11: c4 = c6 and
E12: for b1 being Element of RAT+ holds
( b1 in c3 iff b1 < c6 ) ;
given c7 being Element of RAT+ such that E13: c5 = c7 and
E14: 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 E12;
hence ( not ( c8 < c6 & not c8 < c7 ) & not ( c8 < c7 & not c8 < c6 ) ) by E14;
end;
hence c4 = c5 by E11, E13, E10;
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 E11: 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 E4;
take c6 = c5;
take c7 = c4;
thus c6 = c7 ;
thus for b1 being Element of RAT+ holds
( b1 in c3 iff b1 < c7 ) by E11;
end;
assume E11: 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
E12: 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 E12;
hence c5 < c4 ;
end;
thus ( c5 < c4 implies c5 in c3 ) by E12;
end;
hence not verum by E11;
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 E7;
take c4 ;
thus c4 = c3 ;
end;
consistency
for b1 being Element of REAL+ holds
verum ;
end;

:: deftheorem E11 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 ) ) );

E12: 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 ) ) ) } by XBOOLE_0:def 4;
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;

E13: {} 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;

E14: DEDEKIND_CUTS /\ RAT+ = {{} }
proof
now
let c3 be set ;
thus ( c3 in DEDEKIND_CUTS /\ RAT+ implies c3 = {} )
proof
assume that
E15: c3 in DEDEKIND_CUTS /\ RAT+ and
E16: c3 <> {} ;
E17: c3 in DEDEKIND_CUTS by E15, XBOOLE_0:def 3;
then reconsider c4 = c3 as non empty Subset of RAT+ by E16;
c4 in RAT+ by E15, 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 E17, E12;
end;
thus ( c3 = {} implies c3 in DEDEKIND_CUTS /\ RAT+ ) by E13, XBOOLE_0:def 3;
end;
hence DEDEKIND_CUTS /\ RAT+ = {{} } by TARSKI:def 1;
end;

E15: 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 E16: 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
E17: c3 = c4 and
E18: DEDEKIND_CUT c3 = { b1 where B is Element of RAT+ : b1 < c4 } by E9;
assume E19: c3 <> {} ;
{} <=' c4 by ARYTM_3:71;
then {} < c4 by E17, E19, ARYTM_3:75;
then {} in DEDEKIND_CUT c3 by E18;
hence not verum by E16;
end;
suppose not c3 in RAT+ ;
hence c3 = {} by E16, E9;
end;
end;
end;
E16: for b1 being set holds
not b1 in { b2 where B is Element of RAT+ : b2 < {} }
proof
given c4 being set such that E17: c4 in { b1 where B is Element of RAT+ : b1 < {} } ;
ex b1 being Element of RAT+ st
( b1 = c4 & b1 < {} ) by E17;
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 E9;
hence DEDEKIND_CUT c3 = {} by E16, XBOOLE_0:def 1;
end;

E16: 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 E17: 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 E18: ex b1 being Element of RAT+ st
( GLUED c3 = b1 & ( for b2 being Element of RAT+ holds
( b2 in c3 iff b2 < b1 ) ) ) by E11;
assume c3 <> {} ;
then consider c4 being Element of RAT+ such that
E19: c4 in c3 by SUBSET_1:10;
c4 < {} by E17, E18, E19;
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 E17, E11;
end;
end;
end;
assume E17: 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
E18: GLUED c3 = c4 and
E19: for b1 being Element of RAT+ holds
( b1 in c3 iff b1 < c4 ) by E11;
assume E20: GLUED c3 <> {} ;
{} <=' c4 by ARYTM_3:71;
then {} < c4 by E18, E20, ARYTM_3:75;
hence not verum by E17, E19;
end;

E17: 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
E18: c4 = GLUED c3 and
E19: for b1 being Element of RAT+ holds
( b1 in c3 iff b1 < c4 ) by E11;
consider c5 being Element of RAT+ such that
E20: c4 = c5 and
E21: DEDEKIND_CUT (GLUED c3) = { b1 where B is Element of RAT+ : b1 < c5 } by E18, E9;
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 E21;
hence c6 in c3 by E19, E20;
end;
let c6 be set ; :: according to TARSKI:def 3
assume E22: c6 in c3 ;
then reconsider c7 = c6 as Element of RAT+ ;
c7 < c4 by E19, E22;
hence c6 in DEDEKIND_CUT (GLUED c3) by E20, E21;
end;
suppose E18: c3 = {} ;
then GLUED c3 = {} by E16;
hence DEDEKIND_CUT (GLUED c3) = c3 by E18, E15;
end;
suppose that E18: c3 <> {} and
E19: for b1 being Element of RAT+ holds
not for b2 being Element of RAT+ holds
( b2 in c3 iff b2 < b1 ) ;
E20: GLUED c3 = c3 by E19, E11;
now
assume GLUED c3 in RAT+ ;
then GLUED c3 in RAT+ /\ DEDEKIND_CUTS by E20, XBOOLE_0:def 3;
then GLUED c3 = {} by E14, TARSKI:def 1;
hence not verum by E18, E16;
end;
hence DEDEKIND_CUT (GLUED c3) = c3 by E20, E9;
end;
end;
end;

E18: 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
E19: c3 = c5 and
E20: 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
E21: c4 = c6 and
E22: 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
E23: c7 in c3 and
E24: not c7 in c4 by TARSKI:def 3;
reconsider c8 = c7 as Element of RAT+ by E19, E23;
let c9 be set ; :: according to TARSKI:def 3
assume E25: c9 in c4 ;
then reconsider c10 = c9 as Element of RAT+ by E21;
c10 <=' c8 by E21, E22, E24, E25;
hence c9 in c3 by E19, E20, E23;
end;

definition
let c3, c4 be Element of REAL+ ;
pred c1 <=' c2 means :E19: :: ARYTM_2:def 5
ex b1, b2 being Element of RAT+ st
( a1 = b1 & a2 = b2 & b1 <=' b2 ) if ( a1 in RAT+ & a2 in RAT+ )
a1 in a2 if ( a1 in RAT+ & not a2 in RAT+ )
not a2 in a1 if ( not a1 in RAT+ & a2 in RAT+ )
otherwise a1 c= a2;
consistency
( ( ( c3 in RAT+ & c4 in RAT+ & c3 in RAT+ ) implies ( c4 in RAT+ or ( ex b1, b2 being Element of RAT+ st
( c3 = b1 & c4 = b2 & b1 <=' b2 ) iff c3 in c4 ) ) ) & ( ( c3 in RAT+ & c4 in RAT+ & c4 in RAT+ ) implies ( c3 in RAT+ or ( not ( ex b1, b2 being Element of RAT+ st
( c3 = b1 & c4 = b2 & b1 <=' b2 ) & c4 in c3 ) & not ( not c4 in c3 & ( for b1, b2 being Element of RAT+ holds
not ( c3 = b1 & c4 = b2 & b1 <=' b2 ) ) ) ) ) ) & ( ( c3 in RAT+ & c4 in RAT+ ) implies ( c4 in RAT+ or c3 in RAT+ or ( c3 in c4 iff not c4 in c3 ) ) ) ) ;
connectedness
for b1, b2 being Element of REAL+ holds
( not ( not ( b1 in RAT+ & b2 in RAT+ & ( for b3, b4 being Element of RAT+ holds
not ( b1 = b3 & b2 = b4 & b3 <=' b4 ) ) ) & ( ( b1 in RAT+ ) implies ( b2 in RAT+ or b1 in b2 ) ) & not ( not b1 in RAT+ & b2 in RAT+ & b2 in b1 ) & ( ( ) implies ( ( b1 in RAT+ & b2 in RAT+ ) or ( b1 in RAT+ & not b2 in RAT+ ) or ( not b1 in RAT+ & b2 in RAT+ ) or b1 c= b2 ) ) ) implies ( not ( b2 in RAT+ & b1 in RAT+ & ( for b3, b4 being Element of RAT+ holds
not ( b2 = b3 & b1 = b4 & b3 <=' b4 ) ) ) & ( ( b2 in RAT+ ) implies ( b1 in RAT+ or b2 in b1 ) ) & not ( not b2 in RAT+ & b1 in RAT+ & b1 in b2 ) & ( ( ) implies ( ( b2 in RAT+ & b1 in RAT+ ) or ( b2 in RAT+ & not b1 in RAT+ ) or ( not b2 in RAT+ & b1 in RAT+ ) or b2 c= b1 ) ) ) )
proof
let c5, c6 be Element of REAL+ ;
assume E19: not ( not ( c5 in RAT+ & c6 in RAT+ & ( for b1, b2 being Element of RAT+ holds
not ( c5 = b1 & c6 = b2 & b1 <=' b2 ) ) ) & not ( c5 in RAT+ & not c6 in RAT+ & not c5 in c6 ) & not ( not c5 in RAT+ & c6 in RAT+ & c6 in c5 ) & not ( not ( c5 in RAT+ & c6 in RAT+ ) & not ( c5 in RAT+ & not c6 in RAT+ ) & not ( not c5 in RAT+ & c6 in RAT+ ) & not c5