Step
*
of Lemma
set_lt_is_sp_of_leq_a
∀[p:PosetSig]. ∀[a,b:|p|]. uiff(a <p b;(a ≤ b) ∧ (¬(b ≤ a)))
BY
{ AssertLemma `set_lt_is_sp_of_leq` []
THEN Unfold `strict_part` (-1)
THEN Trivial }
Latex:
Latex:
\mforall{}[p:PosetSig]. \mforall{}[a,b:|p|]. uiff(a <p b;(a \mleq{} b) \mwedge{} (\mneg{}(b \mleq{} a)))
By
Latex:
AssertLemma `set\_lt\_is\_sp\_of\_leq` []
THEN Unfold `strict\_part` (-1)
THEN Trivial
Home
Index