rp-1<

Theorem.

Arguments:

a (obj), b (obj), c (obj),

Hypotheses:

(ceqa)
(aleb)

Assertions:

(cleb)

Proof:

Hyp Ref Line Expr
Hypo1(ceqa)
2(aleb)
1, 2eqt<3(cleb)