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

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

Piotr Rudnicki wrote:
> 
> The way you have defined predicate 'contains' (strange name 
> for what you
> write in the definiens) it has three arguments and from the fact that
> two of them are equal we cannnot infer what you want as with a 
> different definiens it may be not true.

  Here, the predicate 'contains' can be renamed as other name,
  say 'CTS', but phenomenon is the same. The essential problem
  is deduction mechanism,not naming problem. 
  
  J.C. Chen
    
> (Jing Chao) wrote:
> > 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
>