:: by Library Committee

::

:: Received May 29, 2003

:: Copyright (c) 2003-2017 Association of Mizar Users

0 in NAT

;

then reconsider Z = 0 as Element of REAL by NUMBERS:19;

1 in NAT

;

then reconsider J = 1 as Element of REAL by NUMBERS:19;

Lm1: - 0 = 0

proof end;

Lm2: opp Z = 0

proof end;

Lm3: 1 " = 1

proof end;