:: by Andrzej Trybulec

::

:: Received January 1, 1989

:: Copyright (c) 1990-2016 Association of Mizar Users

Lm1: for r, s being Real st ( ( r in REAL+ & s in REAL+ & ex x9, y9 being Element of REAL+ st

( r = x9 & s = y9 & x9 <=' y9 ) ) or ( r in [:{0},REAL+:] & s in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st

( r = [0,x9] & s = [0,y9] & y9 <=' x9 ) ) or ( s in REAL+ & r in [:{0},REAL+:] ) ) holds

r <= s

proof end;

Lm2: for x being Real

for x1, x2 being Element of REAL st x = [*x1,x2*] holds

( x2 = 0 & x = x1 )

proof end;

Lm3: for x9, y9 being Element of REAL

for x, y being Real st x9 = x & y9 = y holds

+ (x9,y9) = x + y

proof end;

Lm4: {} in {{}}

by TARSKI:def 1;

reconsider o = 0 as Element of REAL+ by ARYTM_2:20;

theorem :: AXIOMS:1

for X, Y being Subset of REAL st ( for x, y being Real st x in X & y in Y holds

x <= y ) holds

ex z being Real st

for x, y being Real st x in X & y in Y holds

( x <= z & z <= y )

x <= y ) holds

ex z being Real st

for x, y being Real st x in X & y in Y holds

( x <= z & z <= y )

proof end;

theorem :: AXIOMS:3

for A being Subset of REAL st 0 in A & ( for x being Real st x in A holds

x + 1 in A ) holds

NAT c= A

x + 1 in A ) holds

NAT c= A

proof end;