:: Basic Properties of Real Numbers - Requirements
:: by Library Committee
::
:: Received February 27, 2003
:: Copyright (c) 2003-2015 Association of Mizar Users
Lm1
:
for
x
,
y
being
Real
st
x
<=
y
&
y
<=
x
holds
x
=
y
proof
end;
Lm2
:
for
x
,
y
,
z
being
Real
st
x
<=
y
&
y
<=
z
holds
x
<=
z
proof
end;
theorem
:: REAL:1
for
x
,
y
being
Real
st
x
<=
y
&
x
is
positive
holds
y
is
positive
proof
end;
theorem
:: REAL:2
for
x
,
y
being
Real
st
x
<=
y
&
y
is
negative
holds
x
is
negative
proof
end;
theorem
:: REAL:3
for
x
,
y
being
Real
st
x
<=
y
& not
x
is
negative
holds
not
y
is
negative
proof
end;
theorem
:: REAL:4
for
x
,
y
being
Real
st
x
<=
y
& not
y
is
positive
holds
not
x
is
positive
proof
end;
theorem
:: REAL:5
for
x
,
y
being
Real
st
x
<=
y
& not
y
is
zero
& not
x
is
negative
holds
y
is
positive
proof
end;
theorem
:: REAL:6
for
x
,
y
being
Real
st
x
<=
y
& not
x
is
zero
& not
y
is
positive
holds
x
is
negative
proof
end;
theorem
:: REAL:7
for
x
,
y
being
Real
st not
x
<=
y
& not
x
is
positive
holds
y
is
negative
proof
end;
theorem
:: REAL:8
for
x
,
y
being
Real
st not
x
<=
y
& not
y
is
negative
holds
x
is
positive
proof
end;