:: by Library Committee

::

:: Received February 27, 2003

:: Copyright (c) 2003-2021 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;