[mizar] Mizar 7.8.07 accepts an incorrect inference?

["Chisolm, Bill" <bill.chisolm@intel.com>]

During my efforts to learn Mizar, I have come across an example where
Mizar
appears to accept an invalid inference, without any error message.

Am I misunderstanding some fundamental idea here?  Could this really be
a
bug in the Mizar verifier?

I will insert the short example below.  It contains one scheme, and two 
theorems.  The scheme is correct.  However, each of the theorems
contains an 
error that should be reported by Mizar.  But in fact, Mizar 7.8.07
accepts
this article without any errors.

Bill Chisolm
Intel Corporation
Columbia, South Carolina, USA


Mizar article follows:
- - - - - - - - - - -

environ
 vocabularies ARYTM;
 notations NUMBERS, XXREAL_0, NAT_1;
 constructors XXREAL_0, NAT_1;
 registrations XXREAL_0, ORDINAL1;
 requirements NUMERALS, SUBSET, ARITHM;
 theorems XXREAL_0, NAT_1;

begin

scheme MyScheme { A() -> Nat, B() -> Nat } :
  not ex c being Nat st A() < c & c < B()
provided
  A1: B() = A() + 1
proof
  assume ex c being Nat st A() < c & c < B();
  then consider c being Nat such that
   A2:  A() < c  and
   A3:  c < B();

  A4: A() + 1 <= c by A2, NAT_1:13;
  A() + 1 < B() by A4, A3, XXREAL_0:2;

  hence contradiction by A1;
end;

theorem Th1:    :: Surely there should be an error here somewhere.
  1 = 0
proof
  assume 1 <> 0;

  B1: 3 = 2 + 1;
  B2: not ex c being Nat st 2 < c & c < 3  from MyScheme(B1);
  B3:     ex c being Nat st 2 < c & c < 3  from MyScheme(B1);

  thus contradiction by B2, B3;
end;

theorem Th2:    :: This also deserves an error message.
  for c being Nat holds 2 < c & c < 3
proof
  C1: 3 = 2 + 1;
  thus thesis from MyScheme(C1);
end;