<2tr

Theorem.

Arguments:

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

Hypotheses:

(deqb)
(ceqa)
(aleb)

Assertions:

(cled)

Proof:

Hyp Ref Line Expr
Hypo1(deqb)
2(ceqa)
3(aleb)
2, 3rp-1<4(cleb)
1, 4rp-2<5(cled)