If A=B & (A contains C), why mizar doesn't infer (B contains C)

["Chen, Jing Chao (Jing Chao)" <jchen33@lucent.com>]

Recently, I found that the proof of a very simple proposition cannot be
accpted by Mizar.
For example
definition
 let f, tm be set, t be Subset of tm;
 pred t contains f means
      t c= f;
end;

 for f, tm1 be set, t1 be Subset of tm1,
 tm2 be set, t2 be Subset of tm2 st
    t1 contains f & t1=t2 holds t2 contains f;
::>                 *4
This proposition can be simplified into 
   A=B & (A contains C)  => B contains C.
Clearly, it is ture. However, Mizar presented error 4.
What deduction mechanism doesn't allow such an inference ?

Jingchao Chen