rp-2<

Theorem.

Arguments:

a (st), b (coll), c (coll),

Hypotheses:

(cequivb)
(ainb)

Assertions:

(ainc)

Proof:

Hyp Ref Line Expr
Hypo1(cequivb)
2(ainb)
1eqsym3(bequivc)
2, 3rp-2>4(ainc)