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