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

[bancerek@cs.shinshu-u.ac.jp]

Hi,

In your case Mizar do not knows the meaning of the predicate.
You should read this like

for f, tm1 being set, t1 being Subset of tm1
for tm2 being set, t2 being Subset of tm2
 st  P(f,tm1,t1)  &  t1 = t2
 holds  P(f, tm2, t2);

So, you need "tm1 = tm2" in premisses to have it true.
In case, when P(f, tm, t) means "t <> tm" the statement
will be false.

Grzegorz