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