Step
*
of Lemma
dl-lt_functionality
∀x,y,x',y':dl-Obj(). ((↑dlo_eq(x;x'))
⇒ (↑dlo_eq(y;y'))
⇒ x ≤ y = x' ≤ y')
BY
{ (Auto THEN (RWO "assert-dlo_eq" 5 THENA Auto) THEN (RWO "assert-dlo_eq" 6 THENA Auto) THEN EqCD THEN Auto) }
Latex:
Latex:
\mforall{}x,y,x',y':dl-Obj(). ((\muparrow{}dlo\_eq(x;x')) {}\mRightarrow{} (\muparrow{}dlo\_eq(y;y')) {}\mRightarrow{} x \mleq{} y = x' \mleq{} y')
By
Latex:
(Auto
THEN (RWO "assert-dlo\_eq" 5 THENA Auto)
THEN (RWO "assert-dlo\_eq" 6 THENA Auto)
THEN EqCD
THEN Auto)
Home
Index