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

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

> "Chen, Jing Chao (Jing Chao)" wrote:
>

>
> 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.
>
>   if it may be not true, could you give me such an example ? So
>  far, I cannot find such an example.
>

Just take:

definition
 let f, tm be set, t be Subset of tm;
 pred t contains f means
      t<>tm & t c= f;
end;

Andrzej Trybulec