Step
*
1
1
of Lemma
qoset_lt_trans
1. s : QOSet
⊢ UniformlyTrans(|s|;x,y.strict_part(x,y.x ≤ y;x;y))
BY
{ ((Backchain ``utrans_imp_sp_utrans set_leq_trans``) THEN Auto)⋅ }
Latex:
Latex:
1. s : QOSet
\mvdash{} UniformlyTrans(|s|;x,y.strict\_part(x,y.x \mleq{} y;x;y))
By
Latex:
((Backchain ``utrans\_imp\_sp\_utrans set\_leq\_trans``) THEN Auto)\mcdot{}
Home
Index