---

Step * of Lemma req_fake_le_antisymmetry

No Annotations
∀[x,y:ℝ].  (x = y) supposing ((y ≤ x) and (x ≤ y))
BY
{ (Auto THEN (All (RWO "rleq-iff4") THENA Auto) THEN D 0 THEN Auto THEN ∀h:hyp. (InstHyp [⌜n⌝] h⋅ THENA Auto) ) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[x,y:\mBbbR{}].    (x  =  y)  supposing  ((y  \mleq{}  x)  and  (x  \mleq{}  y))


By

---

Latex:
(Auto
  THEN  (All  (RWO  "rleq-iff4")  THENA  Auto)
  THEN  D  0
  THEN  Auto
  THEN  \mforall{}h:hyp.  (InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  h\mcdot{}  THENA  Auto)  )

---

Home Index