Step
*
1
1
1
of Lemma
natset-subset-natset
1. n : ℕ
2. m : ℕ
3. (natset(n) ⊆ natset(m))
4. (natset(m) ∈ natset(n))
⊢ n ≤ m
BY
{ ((RWO "setsubset-iff" (-2) THENA Auto)
THEN (Assert (natset(m) ∈ natset(m)) BY
Auto)
THEN InstLemma `setmem-irreflexive` [⌜natset(m)⌝]⋅
THEN Auto) }
Latex:
Latex:
1. n : \mBbbN{}
2. m : \mBbbN{}
3. (natset(n) \msubseteq{} natset(m))
4. (natset(m) \mmember{} natset(n))
\mvdash{} n \mleq{} m
By
Latex:
((RWO "setsubset-iff" (-2) THENA Auto)
THEN (Assert (natset(m) \mmember{} natset(m)) BY
Auto)
THEN InstLemma `setmem-irreflexive` [\mkleeneopen{}natset(m)\mkleeneclose{}]\mcdot{}
THEN Auto)
Home
Index