[mizar] Nat not Real trouble

[broderic@ugrad.cs.ualberta.ca]

Hi:

Could someone explain to me why I get this error and how to work around it?

environ

 vocabulary FUNCT_1, FINSEQ_4;
 notation XBOOLE_0, SUBSET_1, REAL_1, FUNCT_2, NAT_1, FINSEQ_4, NUMBERS;
 constructors FINSEQ_4, FUNCT_2;
 clusters FINSET_1, ORDINAL2;

begin

      consider n being Nat;
      n is Real;

    consider X being non empty set;
    consider F being Function of X, NAT;
    consider x being Element of X;
      F/.x is Nat;
      F/.x is Real;
::>              *4

I am using: Mizar Ver. 7.0.07

-- 
Broderick