[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] Why *4?
Hi:
In the following
-----------------------------------------------------------------------------
environ
vocabulary FUNCT_1, RELAT_1, BOOLE;
notation XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS;
constructors FUNCT_2, NUMBERS;
clusters FUNCT_2;
theorems FUNCT_2;
begin
consider f being Function of NAT, NAT;
dom f = NAT by FUNCT_2:def 1;
::> *4
NAT = {} implies NAT = {}; then
dom f = NAT by FUNCT_2:def 1;
------------------------------------------------------------------------------
we get *4. Why? Why adding an obvious premise here solves the problem?
Adding clusters from XBOOLE_0 and ORDINAL2 solves the problem too but this
is not the point.
--
Piotr Rudnicki CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr