---

Step * of Lemma rel_le_refl_cl_sp

∀[T:Type]. ∀[r:T ⟶ T ⟶ ℙ].  (dec_binrel(T;x,y:T. x = y ∈ T) ⇒ r ≡>{T} (r\\00B8) supposing anti_sym(T;r))
BY
{ ((Eval ``dec_binrel xxanti_sym anti_sym 
  refl_cl s_part binrel_le `` 0 
THEN RepD) THENA Auto) }

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[r:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (dec\_binrel(T;x,y:T.  x  =  y)  {}\mRightarrow{}  r  \mequiv{}>\{T\}  (r\mbackslash{}\msupzero{})  supposing  anti\_sym(T;r))


By

---

Latex:
((Eval  ``dec\_binrel  xxanti\_sym  anti\_sym 
    refl\_cl  s\_part  binrel\_le  ``  0 
THEN  RepD)  THENA  Auto)

---

Home Index