:: REAL_1 semantic presentation

begin

registration
cluster  ->  real for Element of REAL ;
coherence
 for b1 being Element of REAL holds b1 is real ;
end;

definition
mode Real is Element of REAL ;
end;

registration
clusterV11() ext-real positive real for Element of REAL ;
existence
 ex b1 being Real st b1 is positive
proof
take  1 ; ::_thesis: 1 is positive
thus  1 is positive ; ::_thesis: verum
end;
end;

definition
let x be Real;
:: original: -
redefine func - x ->  Real;
coherence
 - x is Real by XREAL_0:def_1;
:: original: "
redefine funcx "  ->  Real;
coherence
 x " is Real by XREAL_0:def_1;
end;

definition
let x be real number ;
let y be Real;
:: original: +
redefine funcx + y ->  Real;
coherence
 x + y is Real by XREAL_0:def_1;
:: original: *
redefine funcx * y ->  Real;
coherence
 x * y is Real by XREAL_0:def_1;
:: original: -
redefine funcx - y ->  Real;
coherence
 x - y is Real by XREAL_0:def_1;
:: original: /
redefine funcx / y ->  Real;
coherence
 x / y is Real by XREAL_0:def_1;
end;

definition
let x be Real;
let y be real number ;
:: original: +
redefine funcx + y ->  Real;
coherence
 x + y is Real by XREAL_0:def_1;
:: original: *
redefine funcx * y ->  Real;
coherence
 x * y is Real by XREAL_0:def_1;
:: original: -
redefine funcx - y ->  Real;
coherence
 x - y is Real by XREAL_0:def_1;
:: original: /
redefine funcx / y ->  Real;
coherence
 x / y is Real by XREAL_0:def_1;
end;


theorem :: REAL_1:1
REAL+ =  {  r where r is Real : 0 <= r  }
proof
set RP =  {  r where r is Real : 0 <= r  }  ;
thus  REAL+ c=  {  r where r is Real : 0 <= r  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  r where r is Real : 0 <= r  }  c= REAL+
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in REAL+ or e in  {  r where r is Real : 0 <= r  }  )
assume A1: e in REAL+ ; ::_thesis: e in  {  r where r is Real : 0 <= r  }
then reconsider r = e as Real by ARYTM_0:1;
reconsider o = 0 , s = r as Element of REAL+ by ARYTM_2:20, A1;
 o <=' s by ARYTM_1:6;
then  0 <= r by ARYTM_2:20, XXREAL_0:def_5;
hence  e in  {  r where r is Real : 0 <= r  }  ; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  r where r is Real : 0 <= r  }  or e in REAL+ )
assume  e in  {  r where r is Real : 0 <= r  }  ; ::_thesis: e in REAL+
then A2: ex r being Real st
( e = r & 0 <= r ) ;
 not 0 in [:{0},REAL+:] by ARYTM_0:5, XBOOLE_0:3, ARYTM_2:20;
hence  e in REAL+ by A2, XXREAL_0:def_5; ::_thesis: verum
end;