[mizar] mode definition/"the" question

[Jesse Alama <jesse.alama@gmail.com>]

Consider the vocabulary file

===== [ witness.voc ] =====
MFOO1
MFOO2
===========================

and the article

===== [ witness.miz ] ===============================================
environ

vocabularies TARSKI, XBOOLE_0, WITNESS;
notations TARSKI, XBOOLE_0;
constructors TARSKI, XBOOLE_0;
registrations XBOOLE_0;
theorems TARSKI, XBOOLE_0;

begin

definition
 mode FOO1
 means :DefFOO1:
 ex y being set st it is empty & y is non empty;
 existence
 proof
   A: the non empty set is non empty;
   take the empty set;
   thus thesis by A;
 end;
end;

definition
 mode FOO2
 means :DefFOO2:
 the FOO1 is empty & it is non empty;
 existence by DefFOO1;
end;

Lm1: the FOO1 is empty by DefFOO1;
Lm2: the FOO1 is empty by DefFOO2;
Lm3: ex x being set st the FOO1 is empty by DefFOO2;
Lm4: ex x being set st the FOO1 is empty & x is non empty by DefFOO2;
=====================================================================

My puzzle is that the four theorems at the end are all flagged as *4.  
I put these statements in increasing level of surprisingness.  Any 
explanation for why all of these are rejected by the checker?  (FWIW, 
I'm testing this on mizar 7.12.01-4.166.1132, on darwin.)  I'm actually 
most interesed in why Lm2 is rejected, but all of these are a puzzle to 
me.

Thanks,

Jesse

--
Jesse Alama
http://centria.di.fct.unl.pt/~alama/