Step
*
of Lemma
testnlrst
∀es:EO. ∀A:Type. ((A ⊆r E)
⇒ (∀a,b,c:A. ((a < b)
⇒ (b < c)
⇒ (c < a)
⇒ False)))
BY
{ (UnivCD THENA Auto) }
1
1. es : EO@i'
2. A : Type@i'
3. A ⊆r E@i
4. a : A@i
5. b : A@i
6. c : A@i
7. (a < b)@i
8. (b < c)@i
9. (c < a)@i
⊢ False
Latex:
Latex:
\mforall{}es:EO. \mforall{}A:Type. ((A \msubseteq{}r E) {}\mRightarrow{} (\mforall{}a,b,c:A. ((a < b) {}\mRightarrow{} (b < c) {}\mRightarrow{} (c < a) {}\mRightarrow{} False)))
By
Latex:
(UnivCD THENA Auto)
Home
Index