:: XXREAL_0 semantic presentation

begin

definition
let x be set ;
attrx is ext-real  means :Def1: :: XXREAL_0:def 1
x in ExtREAL ;
end;

:: deftheorem Def1 defines ext-real XXREAL_0:def_1_:_
 for x being set holds
( x is ext-real iff x in ExtREAL );

registration
cluster ext-real for set ;
existence
 ex b1 being number st b1 is ext-real
proof
take  0 ; ::_thesis: 0 is ext-real
thus  0 in ExtREAL by XBOOLE_0:def_3; :: according to XXREAL_0:def_1 ::_thesis: verum
end;
cluster  ->  ext-real for Element of ExtREAL ;
coherence
 for b1 being Element of ExtREAL holds b1 is ext-real by Def1;
end;

registration
ext-real number  ex b1 being set st
for b2 being ext-real number holds b2 in b1
proof
take  ExtREAL ; ::_thesis: for b1 being ext-real number holds b1 in ExtREAL
thus  for b1 being ext-real number holds b1 in ExtREAL by Def1; ::_thesis: verum
end;
end;

definition
func +infty  ->  set  equals :: XXREAL_0:def 2
 REAL ;
coherence
 REAL is set ;
func -infty  ->  set  equals :: XXREAL_0:def 3
[0,REAL];
coherence
 [0,REAL] is set ;
end;

:: deftheorem  defines +infty XXREAL_0:def_2_:_
 +infty = REAL ;

:: deftheorem  defines -infty XXREAL_0:def_3_:_
 -infty = [0,REAL];

definition
redefine func ExtREAL  equals :: XXREAL_0:def 4
REAL \/ {+infty,-infty};
compatibility
 for b1 being set holds
( b1 = ExtREAL iff b1 = REAL \/ {+infty,-infty} ) ;
end;

:: deftheorem  defines ExtREAL XXREAL_0:def_4_:_
 ExtREAL = REAL \/ {+infty,-infty};

registration
cluster +infty  ->  ext-real ;
coherence
 +infty is ext-real
proof
 +infty in {REAL,[0,REAL]} by TARSKI:def_2;
then  +infty in ExtREAL by XBOOLE_0:def_3;
hence  +infty is ext-real ; ::_thesis: verum
end;
cluster -infty  ->  ext-real ;
coherence
 -infty is ext-real
proof
 -infty in {REAL,[0,REAL]} by TARSKI:def_2;
then  -infty in ExtREAL by XBOOLE_0:def_3;
hence  -infty is ext-real ; ::_thesis: verum
end;
end;

definition
let x, y be ext-real number ;
predx <= y means :Def5: :: XXREAL_0:def 5
 ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & x9 <=' y9 ) if ( x in REAL+ & y in REAL+ )
ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & y9 <=' x9 ) if ( x in [:{0},REAL+:] & y in [:{0},REAL+:] )
otherwise ( ( y in REAL+ & x in [:{0},REAL+:] ) or x = -infty or y = +infty );
consistency
 ( x in REAL+ & y in REAL+ & x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & x9 <=' y9 ) iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & y9 <=' x9 ) ) ) by ARYTM_0:5, XBOOLE_0:3;
reflexivity
 for x being ext-real number holds
( ( x in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( x = x9 & x = y9 & x9 <=' y9 ) ) & ( x in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( x = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not x in REAL+ or not x in REAL+ ) & ( not x in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & x in [:{0},REAL+:] ) & not x = -infty implies x = +infty ) )
proof
let x be ext-real number ; ::_thesis: ( ( x in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( x = x9 & x = y9 & x9 <=' y9 ) ) & ( x in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( x = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not x in REAL+ or not x in REAL+ ) & ( not x in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & x in [:{0},REAL+:] ) & not x = -infty implies x = +infty ) )
assume A1: ( ( x in REAL+ & x in REAL+ & ( for x9, y9 being Element of REAL+ holds
( not x = x9 or not x = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & x in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not x = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not x in REAL+ ) & ( not x in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not x = +infty ) ) ; ::_thesis: contradiction
 x in ExtREAL by Def1;
then A2: ( x in (REAL+ \/ [:{0},REAL+:]) \ {[0,0]} or x in {+infty,-infty} ) by XBOOLE_0:def_3;
percases ( ( x in REAL+ & ( for x9, y9 being Element of REAL+ holds
( not x = x9 or not x = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not x = [0,y9] or not y9 <=' x9 ) ) ) or ( not x in REAL+ & not x in [:{0},REAL+:] & not ( x in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not x = +infty ) ) by A1;
supposethat A3: x in REAL+ and
A4: for x9, y9 being Element of REAL+ holds
( not x = x9 or not x = y9 or not x9 <=' y9 ) ; ::_thesis: contradiction
reconsider x9 = x as Element of REAL+ by A3;
 not x9 <=' x9 by A4;
hence  contradiction ; ::_thesis: verum
end;
supposethat A5: x in [:{0},REAL+:] and
A6: for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not x = [0,y9] or not y9 <=' x9 ) ; ::_thesis: contradiction
consider z, x9 being set  such that
A7: z in {0} and
A8: x9 in REAL+ and
A9: x = [z,x9] by A5, ZFMISC_1:84;
reconsider x9 = x9 as Element of REAL+ by A8;
 x = [0,x9] by A7, A9, TARSKI:def_1;
then  not x9 <=' x9 by A6;
hence  contradiction ; ::_thesis: verum
end;
suppose ( not x in REAL+ & not x in [:{0},REAL+:] & not ( x in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not x = +infty ) ; ::_thesis: contradiction
hence  contradiction by A2, TARSKI:def_2, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
connectedness
 for x, y being ext-real number st ( ( x in REAL+ & y in REAL+ & ( for x9, y9 being Element of REAL+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not y = +infty ) ) holds
( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )
proof
let x, y be ext-real number ; ::_thesis: ( ( ( x in REAL+ & y in REAL+ & ( for x9, y9 being Element of REAL+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not y = +infty ) ) implies ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) ) )
assume A10: ( ( x in REAL+ & y in REAL+ & ( for x9, y9 being Element of REAL+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not y = +infty ) ) ; ::_thesis: ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )
 x in ExtREAL by Def1;
then A11: ( x in (REAL+ \/ [:{0},REAL+:]) \ {[0,0]} or x in {+infty,-infty} ) by XBOOLE_0:def_3;
 y in ExtREAL by Def1;
then A12: ( y in (REAL+ \/ [:{0},REAL+:]) \ {[0,0]} or y in {+infty,-infty} ) by XBOOLE_0:def_3;
percases ( ( x in REAL+ & y in REAL+ & ( for x9, y9 being Element of REAL+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not y = +infty ) ) by A10;
supposethat A13: ( x in REAL+ & y in REAL+ ) and
A14: for x9, y9 being Element of REAL+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ; ::_thesis: ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )
hereby  ::_thesis: ( ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )
assume  ( y in REAL+ & x in REAL+ ) ; ::_thesis: ex y9, x9 being Element of REAL+ st
( y = y9 & x = x9 & y9 <=' x9 )
then reconsider x9 = x, y9 = y as Element of REAL+ ;
take y9 = y9; ::_thesis: ex x9 being Element of REAL+ st
( y = y9 & x = x9 & y9 <=' x9 )
take x9 = x9; ::_thesis: ( y = y9 & x = x9 & y9 <=' x9 )
thus  ( y = y9 & x = x9 ) ; ::_thesis: y9 <=' x9
thus  y9 <=' x9 by A14; ::_thesis: verum
end;
thus  ( ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) ) by A13, ARYTM_0:5, XBOOLE_0:3; ::_thesis: verum
end;
supposethat A15: ( x in [:{0},REAL+:] & y in [:{0},REAL+:] ) and
A16: for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ; ::_thesis: ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )
now__::_thesis:_(_y_in_[:{0},REAL+:]_&_x_in_[:{0},REAL+:]_implies_ex_y9,_x9_being_Element_of_REAL+_st_
(_y_=_[0,y9]_&_x_=_[0,x9]_&_x9_<='_y9_)_)
assume  y in [:{0},REAL+:] ; ::_thesis: ( x in [:{0},REAL+:] implies ex y9, x9 being Element of REAL+ st
( y = [0,y9] & x = [0,x9] & x9 <=' y9 ) )
then consider z, y9 being set  such that
A17: z in {0} and
A18: y9 in REAL+ and
A19: y = [z,y9] by ZFMISC_1:84;
A20: z = 0 by A17, TARSKI:def_1;
assume  x in [:{0},REAL+:] ; ::_thesis: ex y9, x9 being Element of REAL+ st
( y = [0,y9] & x = [0,x9] & x9 <=' y9 )
then consider z, x9 being set  such that
A21: z in {0} and
A22: x9 in REAL+ and
A23: x = [z,x9] by ZFMISC_1:84;
reconsider x9 = x9, y9 = y9 as Element of REAL+ by A18, A22;
take y9 = y9; ::_thesis: ex x9 being Element of REAL+ st
( y = [0,y9] & x = [0,x9] & x9 <=' y9 )
take x9 = x9; ::_thesis: ( y = [0,y9] & x = [0,x9] & x9 <=' y9 )
thus  ( y = [0,y9] & x = [0,x9] ) by A17, A19, A21, A23, TARSKI:def_1; ::_thesis: x9 <=' y9
 z = 0 by A21, TARSKI:def_1;
hence  x9 <=' y9 by A16, A19, A20, A23; ::_thesis: verum
end;
hence  ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) ) by A15, ARYTM_0:5, XBOOLE_0:3; ::_thesis: verum
end;
suppose ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not y = +infty ) ; ::_thesis: ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )
hence  ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) ) by A11, A12, TARSKI:def_2, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem Def5 defines <= XXREAL_0:def_5_:_
 for x, y being ext-real number holds
( ( x in REAL+ & y in REAL+ implies ( x <= y iff ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & x9 <=' y9 ) ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( x <= y iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & y9 <=' x9 ) ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) implies ( x <= y iff ( ( y in REAL+ & x in [:{0},REAL+:] ) or x = -infty or y = +infty ) ) ) );


notation
let a, b be ext-real number ;
synonym b >= a for a <= b;
antonym b < a for a <= b;
antonym a > b for a <= b;
end;

Lm1:  +infty <> [0,0]
proof
assume  +infty = [0,0] ; ::_thesis: contradiction
then  +infty = {{0},{0}} by ENUMSET1:29
.= {{0}} by ENUMSET1:29 ;
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;

Lm2:  not +infty in REAL+
by ARYTM_0:1, ORDINAL1:5;

Lm3:  not -infty in REAL+
proof
A1: ( {0,REAL} in -infty & REAL in {0,REAL} ) by TARSKI:def_2;
assume  -infty in REAL+ ; ::_thesis: contradiction
hence  contradiction by A1, ARYTM_0:1, XREGULAR:7; ::_thesis: verum
end;

Lm4:  not +infty in [:{0},REAL+:]
proof
assume  +infty in [:{0},REAL+:] ; ::_thesis: contradiction
then  +infty in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def_3;
then  +infty in REAL by Lm1, ZFMISC_1:56;
hence  contradiction ; ::_thesis: verum
end;

Lm5:  not -infty in [:{0},REAL+:]
proof
assume  -infty in [:{0},REAL+:] ; ::_thesis: contradiction
then  REAL in REAL+ by ZFMISC_1:87;
hence  contradiction by ARYTM_0:1, ORDINAL1:5; ::_thesis: verum
end;

Lm6:  -infty < +infty
proof
 -infty <> +infty by TARSKI:def_2;
hence  -infty < +infty by Def5, Lm3, Lm5; ::_thesis: verum
end;

theorem Th1: :: XXREAL_0:1
for a, b being ext-real number st a <= b & b <= a holds
a = b
proof
let a, b be ext-real number ; ::_thesis: ( a <= b & b <= a implies a = b )
assume that
A1: a <= b and
A2: b <= a ; ::_thesis: a = b
percases ( ( a in REAL+ & b in REAL+ ) or ( a in REAL+ & b in [:{0},REAL+:] ) or ( b in REAL+ & a in [:{0},REAL+:] ) or ( a in [:{0},REAL+:] & b in [:{0},REAL+:] ) or ( ( a = -infty or a = +infty ) & ( b = -infty or b = +infty ) ) or ( ( not a in REAL+ or not b in REAL+ ) & ( not a in [:{0},REAL+:] or not b in [:{0},REAL+:] ) & ( not b in REAL+ or not a in [:{0},REAL+:] ) & ( not a in REAL+ or not b in [:{0},REAL+:] ) ) ) ;
suppose ( a in REAL+ & b in REAL+ ) ; ::_thesis: a = b
then  ( ex a9, b9 being Element of REAL+ st
( a = a9 & b = b9 & a9 <=' b9 ) & ex b99, a99 being Element of REAL+ st
( b = b99 & a = a99 & b99 <=' a99 ) ) by A1, A2, Def5;
hence  a = b by ARYTM_1:4; ::_thesis: verum
end;
supposeA3: ( a in REAL+ & b in [:{0},REAL+:] ) ; ::_thesis: a = b
then  ( not b in REAL+ & not a in [:{0},REAL+:] ) by ARYTM_0:5, XBOOLE_0:3;
hence  a = b by A1, A3, Def5, Lm3, Lm4; ::_thesis: verum
end;
supposeA4: ( b in REAL+ & a in [:{0},REAL+:] ) ; ::_thesis: a = b
then  ( not a in REAL+ & not b in [:{0},REAL+:] ) by ARYTM_0:5, XBOOLE_0:3;
hence  a = b by A2, A4, Def5, Lm3, Lm4; ::_thesis: verum
end;
supposeA5: ( a in [:{0},REAL+:] & b in [:{0},REAL+:] ) ; ::_thesis: a = b
consider a9, b9 being Element of REAL+  such that
A6: ( a = [0,a9] & b = [0,b9] ) and
A7: b9 <=' a9 by A1, A5, Def5;
consider b99, a99 being Element of REAL+  such that
A8: ( b = [0,b99] & a = [0,a99] ) and
A9: a99 <=' b99 by A2, A5, Def5;
 ( a9 = a99 & b9 = b99 ) by A6, A8, XTUPLE_0:1;
hence  a = b by A7, A8, A9, ARYTM_1:4; ::_thesis: verum
end;
suppose ( ( a = -infty or a = +infty ) & ( b = -infty or b = +infty ) ) ; ::_thesis: a = b
hence  a = b by A1, A2, Lm6; ::_thesis: verum
end;
supposethat A10: ( ( not a in REAL+ or not b in REAL+ ) & ( not a in [:{0},REAL+:] or not b in [:{0},REAL+:] ) ) and
A11: ( not b in REAL+ or not a in [:{0},REAL+:] ) and
A12: ( not a in REAL+ or not b in [:{0},REAL+:] ) ; ::_thesis: a = b
 ( a = -infty or b = +infty ) by A1, A10, A11, Def5;
hence  a = b by A2, A10, A12, Def5, Lm6; ::_thesis: verum
end;
end;
end;

Lm7:  for a being ext-real number st -infty >= a holds
a = -infty
proof
let a be ext-real number ; ::_thesis: ( -infty >= a implies a = -infty )
 a >= -infty by Def5, Lm3, Lm5;
hence  ( -infty >= a implies a = -infty ) by Th1; ::_thesis: verum
end;

Lm8:  for a being ext-real number st +infty <= a holds
a = +infty
proof
let a be ext-real number ; ::_thesis: ( +infty <= a implies a = +infty )
 a <= +infty by Def5, Lm2, Lm4;
hence  ( +infty <= a implies a = +infty ) by Th1; ::_thesis: verum
end;

theorem Th2: :: XXREAL_0:2
for a, b, c being ext-real number st a <= b & b <= c holds
a <= c
proof
let a, b, c be ext-real number ; ::_thesis: ( a <= b & b <= c implies a <= c )
assume that
A1: a <= b and
A2: b <= c ; ::_thesis: a <= c
percases ( ( a in REAL+ & b in REAL+ & c in REAL+ ) or ( a in REAL+ & b in [:{0},REAL+:] ) or ( b in REAL+ & c in [:{0},REAL+:] ) or ( a in [:{0},REAL+:] & c in REAL+ ) or ( a in [:{0},REAL+:] & b in [:{0},REAL+:] & c in [:{0},REAL+:] ) or ( ( not a in REAL+ or not b in REAL+ or not c in REAL+ ) & ( not a in REAL+ or not b in [:{0},REAL+:] ) & ( not b in REAL+ or not c in [:{0},REAL+:] ) & ( not a in [:{0},REAL+:] or not c in REAL+ ) & ( not a in [:{0},REAL+:] or not b in [:{0},REAL+:] or not c in [:{0},REAL+:] ) ) ) ;
supposethat A3: a in REAL+ and
A4: b in REAL+ and
A5: c in REAL+ ; ::_thesis: a <= c
consider b99, c9 being Element of REAL+  such that
A6: b = b99 and
A7: c = c9 and
A8: b99 <=' c9 by A2, A4, A5, Def5;
consider a9, b9 being Element of REAL+  such that
A9: a = a9 and
A10: ( b = b9 & a9 <=' b9 ) by A1, A3, A4, Def5;
 a9 <=' c9 by A10, A6, A8, ARYTM_1:3;
hence  a <= c by A5, A9, A7, Def5; ::_thesis: verum
end;
supposeA11: ( a in REAL+ & b in [:{0},REAL+:] ) ; ::_thesis: a <= c
then  ( ( not a in REAL+ or not b in REAL+ ) & ( not a in [:{0},REAL+:] or not b in [:{0},REAL+:] ) ) by ARYTM_0:5, XBOOLE_0:3;
hence  a <= c by A1, A11, Def5, Lm3, Lm4; ::_thesis: verum
end;
supposeA12: ( b in REAL+ & c in [:{0},REAL+:] ) ; ::_thesis: a <= c
then  ( ( not c in REAL+ or not b in REAL+ ) & ( not c in [:{0},REAL+:] or not b in [:{0},REAL+:] ) ) by ARYTM_0:5, XBOOLE_0:3;
hence  a <= c by A2, A12, Def5, Lm3, Lm4; ::_thesis: verum
end;
supposeA13: ( a in [:{0},REAL+:] & c in REAL+ ) ; ::_thesis: a <= c
 ( ( not a in REAL+ or not c in REAL+ ) & ( not a in [:{0},REAL+:] or not c in [:{0},REAL+:] ) ) by A13, ARYTM_0:5, XBOOLE_0:3;
hence  a <= c by A13, Def5; ::_thesis: verum
end;
supposethat A14: a in [:{0},REAL+:] and
A15: b in [:{0},REAL+:] and
A16: c in [:{0},REAL+:] ; ::_thesis: a <= c
consider b99, c9 being Element of REAL+  such that
A17: b = [0,b99] and
A18: c = [0,c9] and
A19: c9 <=' b99 by A2, A15, A16, Def5;
consider a9, b9 being Element of REAL+  such that
A20: a = [0,a9] and
A21: b = [0,b9] and
A22: b9 <=' a9 by A1, A14, A15, Def5;
 b9 = b99 by A21, A17, XTUPLE_0:1;
then  c9 <=' a9 by A22, A19, ARYTM_1:3;
hence  a <= c by A14, A16, A20, A18, Def5; ::_thesis: verum
end;
supposethat A23: ( not a in REAL+ or not b in REAL+ or not c in REAL+ ) and
A24: ( not a in REAL+ or not b in [:{0},REAL+:] ) and
A25: ( not b in REAL+ or not c in [:{0},REAL+:] ) and
A26: ( not a in [:{0},REAL+:] or not c in REAL+ ) and
A27: ( not a in [:{0},REAL+:] or not b in [:{0},REAL+:] or not c in [:{0},REAL+:] ) ; ::_thesis: a <= c
A28: ( b = +infty implies c = +infty ) by A2, Lm8;
A29: ( b = -infty implies a = -infty ) by A1, Lm7;
 ( a = -infty or b = +infty or b = -infty or c = +infty ) by A1, A2, A23, A25, A26, A27, Def5;
hence  a <= c by A1, A2, A23, A24, A25, A27, A28, A29, Def5; ::_thesis: verum
end;
end;
end;

theorem :: XXREAL_0:3
for a being ext-real number holds a <= +infty by Def5, Lm2, Lm4;

theorem :: XXREAL_0:4
for a being ext-real number st +infty <= a holds
a = +infty by Lm8;

theorem :: XXREAL_0:5
for a being ext-real number holds a >= -infty by Def5, Lm3, Lm5;

theorem :: XXREAL_0:6
for a being ext-real number st -infty >= a holds
a = -infty by Lm7;

theorem :: XXREAL_0:7
-infty < +infty by Lm6;

theorem :: XXREAL_0:8
not +infty in REAL ;

Lm9:  for a being ext-real number holds
( a in REAL or a = +infty or a = -infty )
proof
let a be ext-real number ; ::_thesis: ( a in REAL or a = +infty or a = -infty )
 a in ExtREAL by Def1;
then  ( a in REAL or a in {+infty,-infty} ) by XBOOLE_0:def_3;
hence  ( a in REAL or a = +infty or a = -infty ) by TARSKI:def_2; ::_thesis: verum
end;

theorem Th9: :: XXREAL_0:9
for a being ext-real number st a in REAL holds
+infty > a
proof
let a be ext-real number ; ::_thesis: ( a in REAL implies +infty > a )
assume  a in REAL ; ::_thesis: +infty > a
then A1: a <> +infty ;
 +infty >= a by Def5, Lm2, Lm4;
hence  +infty > a by A1, Th1; ::_thesis: verum
end;

theorem Th10: :: XXREAL_0:10
for a, b being ext-real number st a in REAL & b >= a & not b in REAL holds
b = +infty
proof
let a, b be ext-real number ; ::_thesis: ( a in REAL & b >= a & not b in REAL implies b = +infty )
assume that
A1: a in REAL and
A2: b >= a ; ::_thesis: ( b in REAL or b = +infty )
assume A3: not b in REAL ; ::_thesis: b = +infty
 ( b = -infty implies a = -infty ) by A2, Lm7;
hence  b = +infty by A1, A3, Lm9; ::_thesis: verum
end;

theorem Th11: :: XXREAL_0:11
not -infty in REAL
proof
A1: ( {0,REAL} in {{0,REAL},{0}} & REAL in {0,REAL} ) by TARSKI:def_2;
assume  -infty in REAL ; ::_thesis: contradiction
hence  contradiction by A1, XREGULAR:7; ::_thesis: verum
end;

theorem Th12: :: XXREAL_0:12
for a being ext-real number st a in REAL holds
-infty < a
proof
let a be ext-real number ; ::_thesis: ( a in REAL implies -infty < a )
 -infty <= a by Def5, Lm3, Lm5;
hence  ( a in REAL implies -infty < a ) by Th1, Th11; ::_thesis: verum
end;

theorem Th13: :: XXREAL_0:13
for a, b being ext-real number st a in REAL & b <= a & not b in REAL holds
b = -infty
proof
let a, b be ext-real number ; ::_thesis: ( a in REAL & b <= a & not b in REAL implies b = -infty )
assume that
A1: a in REAL and
A2: b <= a ; ::_thesis: ( b in REAL or b = -infty )
assume A3: not b in REAL ; ::_thesis: b = -infty
 ( b = +infty implies a = +infty ) by A2, Lm8;
hence  b = -infty by A1, A3, Lm9; ::_thesis: verum
end;

theorem :: XXREAL_0:14
for a being ext-real number holds
( a in REAL or a = +infty or a = -infty ) by Lm9;

begin

registration
cluster natural  ->  ext-real for set ;
coherence
 for b1 being number st b1 is natural holds
b1 is ext-real
proof
let a be number ; ::_thesis: ( a is natural implies a is ext-real )
assume  a is natural ; ::_thesis: a is ext-real
then  a in NAT by ORDINAL1:def_12;
hence  a in ExtREAL by XBOOLE_0:def_3; :: according to XXREAL_0:def_1 ::_thesis: verum
end;
end;

notation
let a be number ;
synonym  zero a for  empty ;
end;

definition
let a be ext-real number ;
attra is positive  means :: XXREAL_0:def 6
a > 0 ;
attra is negative  means :: XXREAL_0:def 7
a < 0 ;
redefine attr a is empty  means :: XXREAL_0:def 8
a = 0 ;
compatibility
 ( a is zero iff a = 0 ) ;
end;

:: deftheorem  defines positive XXREAL_0:def_6_:_
 for a being ext-real number holds
( a is positive iff a > 0 );

:: deftheorem  defines negative XXREAL_0:def_7_:_
 for a being ext-real number holds
( a is negative iff a < 0 );

:: deftheorem  defines zero XXREAL_0:def_8_:_
 for a being ext-real number holds
( a is zero iff a = 0 );

registration
cluster ext-real positive  ->  non zero ext-real non negative for set ;
coherence
 for b1 being ext-real number st b1 is positive holds
( not b1 is negative & not b1 is zero )
proof
let r be ext-real number ; ::_thesis: ( r is positive implies ( not r is negative & not r is zero ) )
assume  r > 0 ; :: according to XXREAL_0:def_6 ::_thesis: ( not r is negative & not r is zero )
hence  ( r >= 0 & r <> 0 ) ; :: according to XXREAL_0:def_7,XXREAL_0:def_8 ::_thesis: verum
end;
cluster non zero ext-real non negative  ->  ext-real positive for set ;
coherence
 for b1 being ext-real number st not b1 is negative & not b1 is zero holds
b1 is positive
proof
let r be ext-real number ; ::_thesis: ( not r is negative & not r is zero implies r is positive )
assume  ( r >= 0 & r <> 0 ) ; :: according to XXREAL_0:def_7,XXREAL_0:def_8 ::_thesis: r is positive
hence  r > 0 by Th1; :: according to XXREAL_0:def_6 ::_thesis: verum
end;
cluster ext-real negative  ->  non zero ext-real non positive for set ;
coherence
 for b1 being ext-real number st b1 is negative holds
( not b1 is positive & not b1 is zero )
proof
let r be ext-real number ; ::_thesis: ( r is negative implies ( not r is positive & not r is zero ) )
assume  r < 0 ; :: according to XXREAL_0:def_7 ::_thesis: ( not r is positive & not r is zero )
hence  ( r <= 0 & r <> {} ) ; :: according to XXREAL_0:def_6,XXREAL_0:def_8 ::_thesis: verum
end;
cluster non zero ext-real non positive  ->  ext-real negative for set ;
coherence
 for b1 being ext-real number st not b1 is positive & not b1 is zero holds
b1 is negative ;
cluster zero ext-real  ->  ext-real non positive non negative for set ;
coherence
 for b1 being ext-real number st b1 is zero holds
( not b1 is negative & not b1 is positive ) ;
cluster ext-real non positive non negative  ->  zero ext-real for set ;
coherence
 for b1 being ext-real number st not b1 is negative & not b1 is positive holds
b1 is zero ;
end;

registration
cluster +infty  ->  positive ;
coherence
 +infty is positive
proof
thus  0 < +infty by Th9; :: according to XXREAL_0:def_6 ::_thesis: verum
end;
cluster -infty  ->  negative ;
coherence
 -infty is negative
proof
thus  0 > -infty by Th12; :: according to XXREAL_0:def_7 ::_thesis: verum
end;
end;

registration
cluster ext-real positive for set ;
existence
 ex b1 being ext-real number st b1 is positive
proof
take  +infty ; ::_thesis: +infty is positive
thus  +infty is positive ; ::_thesis: verum
end;
cluster ext-real negative for set ;
existence
 ex b1 being ext-real number st b1 is negative
proof
take  -infty ; ::_thesis: -infty is negative
thus  -infty is negative ; ::_thesis: verum
end;
cluster zero ext-real for set ;
existence
 ex b1 being ext-real number st b1 is zero
proof
reconsider z = 0 as ext-real number ;
take  z ; ::_thesis: z is zero
thus  z = 0 ; :: according to XXREAL_0:def_8 ::_thesis: verum
end;
end;

begin

definition
let a, b be ext-real number ;
func min (a,b) ->  set  equals :Def9: :: XXREAL_0:def 9
a if a <= b
otherwise b;
correctness
coherence
( ( a <= b implies a is set ) & ( not a <= b implies b is set ) );
consistency
for b1 being set holds verum;
;
commutativity
 for b1 being set
for a, b being ext-real number st ( a <= b implies b1 = a ) & ( not a <= b implies b1 = b ) holds
( ( b <= a implies b1 = b ) & ( not b <= a implies b1 = a ) ) by Th1;
idempotence
 for a being ext-real number holds
( ( a <= a implies a = a ) & ( not a <= a implies a = a ) ) ;
func max (a,b) ->  set  equals :Def10: :: XXREAL_0:def 10
a if b <= a
otherwise b;
correctness
coherence
( ( b <= a implies a is set ) & ( not b <= a implies b is set ) );
consistency
for b1 being set holds verum;
;
commutativity
 for b1 being set
for a, b being ext-real number st ( b <= a implies b1 = a ) & ( not b <= a implies b1 = b ) holds
( ( a <= b implies b1 = b ) & ( not a <= b implies b1 = a ) ) by Th1;
idempotence
 for a being ext-real number holds
( ( a <= a implies a = a ) & ( not a <= a implies a = a ) ) ;
end;

:: deftheorem Def9 defines min XXREAL_0:def_9_:_
 for a, b being ext-real number holds
( ( a <= b implies min (a,b) = a ) & ( not a <= b implies min (a,b) = b ) );

:: deftheorem Def10 defines max XXREAL_0:def_10_:_
 for a, b being ext-real number holds
( ( b <= a implies max (a,b) = a ) & ( not b <= a implies max (a,b) = b ) );

theorem :: XXREAL_0:15
for a, b being ext-real number holds
( min (a,b) = a or min (a,b) = b ) by Def9;

theorem :: XXREAL_0:16
for a, b being ext-real number holds
( max (a,b) = a or max (a,b) = b ) by Def10;

registration
let a, b be ext-real number ;
cluster min (a,b) ->  ext-real ;
coherence
 min (a,b) is ext-real by Def9;
cluster max (a,b) ->  ext-real ;
coherence
 max (a,b) is ext-real by Def10;
end;

theorem Th17: :: XXREAL_0:17
for a, b being ext-real number holds min (a,b) <= a
proof
let a, b be ext-real number ; ::_thesis: min (a,b) <= a
 ( a <= b or not a <= b ) ;
hence  min (a,b) <= a by Def9; ::_thesis: verum
end;

theorem Th18: :: XXREAL_0:18
for a, b, c, d being ext-real number st a <= b & c <= d holds
min (a,c) <= min (b,d)
proof
let a, b, c, d be ext-real number ; ::_thesis: ( a <= b & c <= d implies min (a,c) <= min (b,d) )
assume that
A1: a <= b and
A2: c <= d ; ::_thesis: min (a,c) <= min (b,d)
 min (a,c) <= c by Th17;
then A3: min (a,c) <= d by A2, Th2;
 min (a,c) <= a by Th17;
then  min (a,c) <= b by A1, Th2;
hence  min (a,c) <= min (b,d) by A3, Def9; ::_thesis: verum
end;

theorem :: XXREAL_0:19
for a, b, c, d being ext-real number st a < b & c < d holds
min (a,c) < min (b,d)
proof
let a, b, c, d be ext-real number ; ::_thesis: ( a < b & c < d implies min (a,c) < min (b,d) )
assume that
A1: a < b and
A2: c < d ; ::_thesis: min (a,c) < min (b,d)
 min (a,c) <= c by Th17;
then A3: min (a,c) < d by A2, Th2;
 min (a,c) <= a by Th17;
then  min (a,c) < b by A1, Th2;
hence  min (a,c) < min (b,d) by A3, Def9; ::_thesis: verum
end;

theorem :: XXREAL_0:20
for a, b, c being ext-real number st a <= b & a <= c holds
a <= min (b,c) by Def9;

theorem :: XXREAL_0:21
for a, b, c being ext-real number st a < b & a < c holds
a < min (b,c) by Def9;

theorem :: XXREAL_0:22
for a, b, c being ext-real number st a <= min (b,c) holds
a <= b
proof
let a, b, c be ext-real number ; ::_thesis: ( a <= min (b,c) implies a <= b )
 min (b,c) <= b by Th17;
hence  ( a <= min (b,c) implies a <= b ) by Th2; ::_thesis: verum
end;

theorem :: XXREAL_0:23
for a, b, c being ext-real number st a < min (b,c) holds
a < b
proof
let a, b, c be ext-real number ; ::_thesis: ( a < min (b,c) implies a < b )
 min (b,c) <= b by Th17;
hence  ( a < min (b,c) implies a < b ) by Th2; ::_thesis: verum
end;

theorem :: XXREAL_0:24
for c, a, b being ext-real number st c <= a & c <= b & ( for d being ext-real number st d <= a & d <= b holds
d <= c ) holds
c = min (a,b)
proof
let c, a, b be ext-real number ; ::_thesis: ( c <= a & c <= b & ( for d being ext-real number st d <= a & d <= b holds
d <= c ) implies c = min (a,b) )
assume that
A1: ( c <= a & c <= b ) and
A2: for d being ext-real number st d <= a & d <= b holds
d <= c ; ::_thesis: c = min (a,b)
 ( min (a,b) <= a & min (a,b) <= b ) by Th17;
then A3: min (a,b) <= c by A2;
 c <= min (a,b) by A1, Def9;
hence  c = min (a,b) by A3, Th1; ::_thesis: verum
end;

theorem Th25: :: XXREAL_0:25
for a, b being ext-real number holds a <= max (a,b)
proof
let a, b be ext-real number ; ::_thesis: a <= max (a,b)
 ( a <= b or not a <= b ) ;
hence  a <= max (a,b) by Def10; ::_thesis: verum
end;

theorem Th26: :: XXREAL_0:26
for a, b, c, d being ext-real number st a <= b & c <= d holds
max (a,c) <= max (b,d)
proof
let a, b, c, d be ext-real number ; ::_thesis: ( a <= b & c <= d implies max (a,c) <= max (b,d) )
assume that
A1: a <= b and
A2: c <= d ; ::_thesis: max (a,c) <= max (b,d)
 d <= max (b,d) by Th25;
then A3: c <= max (b,d) by A2, Th2;
 b <= max (b,d) by Th25;
then  a <= max (b,d) by A1, Th2;
hence  max (a,c) <= max (b,d) by A3, Def10; ::_thesis: verum
end;

theorem :: XXREAL_0:27
for a, b, c, d being ext-real number st a < b & c < d holds
max (a,c) < max (b,d)
proof
let a, b, c, d be ext-real number ; ::_thesis: ( a < b & c < d implies max (a,c) < max (b,d) )
assume that
A1: a < b and
A2: c < d ; ::_thesis: max (a,c) < max (b,d)
 d <= max (b,d) by Th25;
then A3: c < max (b,d) by A2, Th2;
 b <= max (b,d) by Th25;
then  a < max (b,d) by A1, Th2;
hence  max (a,c) < max (b,d) by A3, Def10; ::_thesis: verum
end;

theorem :: XXREAL_0:28
for b, a, c being ext-real number st b <= a & c <= a holds
max (b,c) <= a by Def10;

theorem :: XXREAL_0:29
for b, a, c being ext-real number st b < a & c < a holds
max (b,c) < a by Def10;

theorem :: XXREAL_0:30
for b, c, a being ext-real number st max (b,c) <= a holds
b <= a
proof
let b, c, a be ext-real number ; ::_thesis: ( max (b,c) <= a implies b <= a )
 b <= max (b,c) by Th25;
hence  ( max (b,c) <= a implies b <= a ) by Th2; ::_thesis: verum
end;

theorem :: XXREAL_0:31
for b, c, a being ext-real number st max (b,c) < a holds
b < a
proof
let b, c, a be ext-real number ; ::_thesis: ( max (b,c) < a implies b < a )
 b <= max (b,c) by Th25;
hence  ( max (b,c) < a implies b < a ) by Th2; ::_thesis: verum
end;

theorem :: XXREAL_0:32
for a, c, b being ext-real number st a <= c & b <= c & ( for d being ext-real number st a <= d & b <= d holds
c <= d ) holds
c = max (a,b)
proof
let a, c, b be ext-real number ; ::_thesis: ( a <= c & b <= c & ( for d being ext-real number st a <= d & b <= d holds
c <= d ) implies c = max (a,b) )
assume that
A1: ( a <= c & b <= c ) and
A2: for d being ext-real number st a <= d & b <= d holds
c <= d ; ::_thesis: c = max (a,b)
 ( a <= max (a,b) & b <= max (a,b) ) by Th25;
then A3: c <= max (a,b) by A2;
 max (a,b) <= c by A1, Def10;
hence  c = max (a,b) by A3, Th1; ::_thesis: verum
end;

theorem :: XXREAL_0:33
for a, b, c being ext-real number holds min ((min (a,b)),c) = min (a,(min (b,c)))
proof
let a, b, c be ext-real number ; ::_thesis: min ((min (a,b)),c) = min (a,(min (b,c)))
percases ( ( a <= b & a <= c ) or ( b <= a & b <= c ) or ( c <= b & c <= a ) ) by Th2;
suppose ( a <= b & a <= c ) ; ::_thesis: min ((min (a,b)),c) = min (a,(min (b,c)))
then  ( min (a,b) = a & min (a,c) = a ) by Def9;
hence  min ((min (a,b)),c) = min (a,(min (b,c))) by Def9; ::_thesis: verum
end;
suppose ( b <= a & b <= c ) ; ::_thesis: min ((min (a,b)),c) = min (a,(min (b,c)))
then  ( min (a,b) = b & min (b,c) = b ) by Def9;
hence  min ((min (a,b)),c) = min (a,(min (b,c))) ; ::_thesis: verum
end;
suppose ( c <= b & c <= a ) ; ::_thesis: min ((min (a,b)),c) = min (a,(min (b,c)))
then  ( min (b,c) = c & min (a,c) = c ) by Def9;
hence  min ((min (a,b)),c) = min (a,(min (b,c))) by Def9; ::_thesis: verum
end;
end;
end;

theorem :: XXREAL_0:34
for a, b, c being ext-real number holds max ((max (a,b)),c) = max (a,(max (b,c)))
proof
let a, b, c be ext-real number ; ::_thesis: max ((max (a,b)),c) = max (a,(max (b,c)))
percases ( ( a <= b & a <= c ) or ( b <= a & b <= c ) or ( c <= b & c <= a ) ) by Th2;
supposeA1: ( a <= b & a <= c ) ; ::_thesis: max ((max (a,b)),c) = max (a,(max (b,c)))
A2: ( max (b,c) = b or max (b,c) = c ) by Def10;
 max (a,b) = b by A1, Def10;
hence  max ((max (a,b)),c) = max (a,(max (b,c))) by A1, A2, Def10; ::_thesis: verum
end;
supposeA3: ( b <= a & b <= c ) ; ::_thesis: max ((max (a,b)),c) = max (a,(max (b,c)))
then  max (a,b) = a by Def10;
hence  max ((max (a,b)),c) = max (a,(max (b,c))) by A3, Def10; ::_thesis: verum
end;
supposeA4: ( c <= b & c <= a ) ; ::_thesis: max ((max (a,b)),c) = max (a,(max (b,c)))
A5: ( max (a,b) = b or max (a,b) = a ) by Def10;
 max (b,c) = b by A4, Def10;
hence  max ((max (a,b)),c) = max (a,(max (b,c))) by A4, A5, Def10; ::_thesis: verum
end;
end;
end;

theorem :: XXREAL_0:35
for a, b being ext-real number holds min ((max (a,b)),b) = b
proof
let a, b be ext-real number ; ::_thesis: min ((max (a,b)),b) = b
 b <= max (a,b) by Th25;
hence  min ((max (a,b)),b) = b by Def9; ::_thesis: verum
end;

theorem :: XXREAL_0:36
for a, b being ext-real number holds max ((min (a,b)),b) = b
proof
let a, b be ext-real number ; ::_thesis: max ((min (a,b)),b) = b
 min (a,b) <= b by Th17;
hence  max ((min (a,b)),b) = b by Def10; ::_thesis: verum
end;

theorem Th37: :: XXREAL_0:37
for a, c, b being ext-real number st a <= c holds
max (a,(min (b,c))) = min ((max (a,b)),c)
proof
let a, c, b be ext-real number ; ::_thesis: ( a <= c implies max (a,(min (b,c))) = min ((max (a,b)),c) )
assume A1: a <= c ; ::_thesis: max (a,(min (b,c))) = min ((max (a,b)),c)
percases ( a <= b or b <= a ) ;
supposeA2: a <= b ; ::_thesis: max (a,(min (b,c))) = min ((max (a,b)),c)
then  a <= min (b,c) by A1, Def9;
hence  max (a,(min (b,c))) = min (b,c) by Def10
.= min ((max (a,b)),c) by A2, Def10 ;
::_thesis: verum
end;
supposeA3: b <= a ; ::_thesis: max (a,(min (b,c))) = min ((max (a,b)),c)
then  b <= c by A1, Th2;
hence  max (a,(min (b,c))) = max (a,b) by Def9
.= a by A3, Def10
.= min (a,c) by A1, Def9
.= min ((max (a,b)),c) by A3, Def10 ;
::_thesis: verum
end;
end;
end;

theorem :: XXREAL_0:38
for a, b, c being ext-real number holds min (a,(max (b,c))) = max ((min (a,b)),(min (a,c)))
proof
let a, b, c be ext-real number ; ::_thesis: min (a,(max (b,c))) = max ((min (a,b)),(min (a,c)))
percases ( b <= c or c <= b ) ;
supposeA1: b <= c ; ::_thesis: min (a,(max (b,c))) = max ((min (a,b)),(min (a,c)))
then A2: min (a,b) <= min (a,c) by Th18;
thus  min (a,(max (b,c))) = min (a,c) by A1, Def10
.= max ((min (a,b)),(min (a,c))) by A2, Def10 ; ::_thesis: verum
end;
supposeA3: c <= b ; ::_thesis: min (a,(max (b,c))) = max ((min (a,b)),(min (a,c)))
then A4: min (a,c) <= min (a,b) by Th18;
thus  min (a,(max (b,c))) = min (a,b) by A3, Def10
.= max ((min (a,b)),(min (a,c))) by A4, Def10 ; ::_thesis: verum
end;
end;
end;

theorem :: XXREAL_0:39
for a, b, c being ext-real number holds max (a,(min (b,c))) = min ((max (a,b)),(max (a,c)))
proof
let a, b, c be ext-real number ; ::_thesis: max (a,(min (b,c))) = min ((max (a,b)),(max (a,c)))
percases ( b <= c or c <= b ) ;
supposeA1: b <= c ; ::_thesis: max (a,(min (b,c))) = min ((max (a,b)),(max (a,c)))
then A2: max (a,b) <= max (a,c) by Th26;
thus  max (a,(min (b,c))) = max (a,b) by A1, Def9
.= min ((max (a,b)),(max (a,c))) by A2, Def9 ; ::_thesis: verum
end;
supposeA3: c <= b ; ::_thesis: max (a,(min (b,c))) = min ((max (a,b)),(max (a,c)))
then A4: max (a,c) <= max (a,b) by Th26;
thus  max (a,(min (b,c))) = max (a,c) by A3, Def9
.= min ((max (a,b)),(max (a,c))) by A4, Def9 ; ::_thesis: verum
end;
end;
end;

theorem :: XXREAL_0:40
for a, b, c being ext-real number holds max ((max ((min (a,b)),(min (b,c)))),(min (c,a))) = min ((min ((max (a,b)),(max (b,c)))),(max (c,a)))
proof
let a, b, c be ext-real number ; ::_thesis: max ((max ((min (a,b)),(min (b,c)))),(min (c,a))) = min ((min ((max (a,b)),(max (b,c)))),(max (c,a)))
percases ( a <= c or c <= a ) ;
supposeA1: a <= c ; ::_thesis: max ((max ((min (a,b)),(min (b,c)))),(min (c,a))) = min ((min ((max (a,b)),(max (b,c)))),(max (c,a)))
then A2: max (a,b) <= max (b,c) by Th26;
 min (a,b) <= min (b,c) by A1, Th18;
hence  max ((max ((min (a,b)),(min (b,c)))),(min (c,a))) = max ((min (b,c)),(min (c,a))) by Def10
.= max ((min (b,c)),a) by A1, Def9
.= min ((max (a,b)),c) by A1, Th37
.= min ((max (a,b)),(max (c,a))) by A1, Def10
.= min ((min ((max (a,b)),(max (b,c)))),(max (c,a))) by A2, Def9 ;
::_thesis: verum
end;
supposeA3: c <= a ; ::_thesis: max ((max ((min (a,b)),(min (b,c)))),(min (c,a))) = min ((min ((max (a,b)),(max (b,c)))),(max (c,a)))
then A4: max (a,b) >= max (b,c) by Th26;
 min (a,b) >= min (b,c) by A3, Th18;
hence  max ((max ((min (a,b)),(min (b,c)))),(min (c,a))) = max ((min (a,b)),(min (c,a))) by Def10
.= max ((min (a,b)),c) by A3, Def9
.= min ((max (c,b)),a) by A3, Th37
.= min ((max (c,b)),(max (c,a))) by A3, Def10
.= min ((min ((max (a,b)),(max (b,c)))),(max (c,a))) by A4, Def9 ;
::_thesis: verum
end;
end;
end;

theorem :: XXREAL_0:41
for a being ext-real number holds max (a,+infty) = +infty
proof
let a be ext-real number ; ::_thesis: max (a,+infty) = +infty
 a <= +infty by Def5, Lm2, Lm4;
hence  max (a,+infty) = +infty by Def10; ::_thesis: verum
end;

theorem :: XXREAL_0:42
for a being ext-real number holds min (a,+infty) = a
proof
let a be ext-real number ; ::_thesis: min (a,+infty) = a
 a <= +infty by Def5, Lm2, Lm4;
hence  min (a,+infty) = a by Def9; ::_thesis: verum
end;

theorem :: XXREAL_0:43
for a being ext-real number holds max (a,-infty) = a
proof
let a be ext-real number ; ::_thesis: max (a,-infty) = a
 a >= -infty by Def5, Lm3, Lm5;
hence  max (a,-infty) = a by Def10; ::_thesis: verum
end;

theorem :: XXREAL_0:44
for a being ext-real number holds min (a,-infty) = -infty
proof
let a be ext-real number ; ::_thesis: min (a,-infty) = -infty
 a >= -infty by Def5, Lm3, Lm5;
hence  min (a,-infty) = -infty by Def9; ::_thesis: verum
end;

begin

theorem :: XXREAL_0:45
for a, c, b being ext-real number st a in REAL & c in REAL & a <= b & b <= c holds
b in REAL
proof
let a, c, b be ext-real number ; ::_thesis: ( a in REAL & c in REAL & a <= b & b <= c implies b in REAL )
assume that
A1: a in REAL and
A2: c in REAL and
A3: a <= b and
A4: b <= c ; ::_thesis: b in REAL
 ( b in REAL or b = +infty ) by A1, A3, Th10;
hence  b in REAL by A2, A4, Th13; ::_thesis: verum
end;

theorem :: XXREAL_0:46
for a, b, c being ext-real number st a in REAL & a <= b & b < c holds
b in REAL
proof
let a, b, c be ext-real number ; ::_thesis: ( a in REAL & a <= b & b < c implies b in REAL )
assume that
A1: ( a in REAL & a <= b ) and
A2: b < c ; ::_thesis: b in REAL
 ( b in REAL or b = +infty ) by A1, Th10;
hence  b in REAL by A2, Lm8; ::_thesis: verum
end;

theorem :: XXREAL_0:47
for c, a, b being ext-real number st c in REAL & a < b & b <= c holds
b in REAL
proof
let c, a, b be ext-real number ; ::_thesis: ( c in REAL & a < b & b <= c implies b in REAL )
assume that
A1: c in REAL and
A2: a < b and
A3: b <= c ; ::_thesis: b in REAL
 ( b in REAL or b = -infty ) by A1, A3, Th13;
hence  b in REAL by A2, Lm7; ::_thesis: verum
end;

theorem :: XXREAL_0:48
for a, b, c being ext-real number st a < b & b < c holds
b in REAL
proof
let a, b, c be ext-real number ; ::_thesis: ( a < b & b < c implies b in REAL )
assume A1: ( a < b & b < c ) ; ::_thesis: b in REAL
 ( b in REAL or b = +infty or b = -infty ) by Lm9;
hence  b in REAL by A1, Lm7, Lm8; ::_thesis: verum
end;

definition
let x, y be ext-real number ;
let a, b be set ;
func IFGT (x,y,a,b) ->  set  equals :Def11: :: XXREAL_0:def 11
a if x > y
otherwise b;
correctness
coherence
( ( x > y implies a is set ) & ( not x > y implies b is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def11 defines IFGT XXREAL_0:def_11_:_
 for x, y being ext-real number
for a, b being set holds
( ( x > y implies IFGT (x,y,a,b) = a ) & ( not x > y implies IFGT (x,y,a,b) = b ) );

registration
let x, y be ext-real number ;
let a, b be Nat;
cluster IFGT (x,y,a,b) ->  natural ;
coherence
 IFGT (x,y,a,b) is natural by Def11;
end;

theorem :: XXREAL_0:49
for a, b being ext-real number st max (a,b) <= a holds
max (a,b) = a
proof
let a, b be ext-real number ; ::_thesis: ( max (a,b) <= a implies max (a,b) = a )
assume  max (a,b) <= a ; ::_thesis: max (a,b) = a
then  ( max (a,b) < a or max (a,b) = a ) by Th1;
hence  max (a,b) = a by Th25; ::_thesis: verum
end;

theorem :: XXREAL_0:50
for a, b being ext-real number st a <= min (a,b) holds
min (a,b) = a
proof
let a, b be ext-real number ; ::_thesis: ( a <= min (a,b) implies min (a,b) = a )
assume  min (a,b) >= a ; ::_thesis: min (a,b) = a
then  ( min (a,b) > a or min (a,b) = a ) by Th1;
hence  min (a,b) = a by Th17; ::_thesis: verum
end;