---

Step * of Lemma rel_le_sp_refl_cl

∀[T:Type]. ∀[r:T ⟶ T ⟶ ℙ].  (r ≡>{T} (ro\)) supposing (st_anti_sym(T;r) and irrefl(T;r))
BY
{ ((Eval ``refl_cl s_part xxst_anti_sym st_anti_sym 
 xxirrefl irrefl binrel_le`` 0 THEN RepD ) THENA Auto) }

1
1. [T] : Type
2. [r] : T ⟶ T ⟶ ℙ
3. ∀[a:T]. (¬(r a a))
4. ∀x,y:T.  (¬((r x y) ∧ (r y x)))
5. x : T@i
6. y : T@i
7. r x y@i
⊢ ((x = y ∈ T) ∨ (r x y)) ∧ (¬((y = x ∈ T) ∨ (r y x)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[r:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (r  \mequiv{}>\{T\}  (r\msupzero{}\mbackslash{}))  supposing  (st\_anti\_sym(T;r)  and  irrefl(T;r))


By

---

Latex:
((Eval  ``refl\_cl  s\_part  xxst\_anti\_sym  st\_anti\_sym 
  xxirrefl  irrefl  binrel\_le``  0  THEN  RepD  )  THENA  Auto)

---

Home Index