mode definition/"the" question

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/