Step
*
1
of Lemma
set_leq_trans
1. s : QOSet
2. a : |s|
3. b : |s|
4. c : |s|
5. a ≤ b@i
6. b ≤ c@i
⊢ a ≤ c
BY
{ ((FLemma `qoset_trans` [-1;-2]) THEN Auto) }
Latex:
Latex:
1. s : QOSet
2. a : |s|
3. b : |s|
4. c : |s|
5. a \mleq{} b@i
6. b \mleq{} c@i
\mvdash{} a \mleq{} c
By
Latex:
((FLemma `qoset\_trans` [-1;-2]) THEN Auto)
Home
Index