rp-1>

Theorem.

Arguments:

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

Hypotheses:

(aeqc)
(aleb)

Assertions:

(cleb)

Proof:

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