Step
*
of Lemma
subtype_rel_poset
PosetSig ⊆r PosetSig{[i | j]}
BY
{ (Unfold `poset_sig` 0 THEN Auto) }
Latex:
Latex:
PosetSig  \msubseteq{}r  PosetSig\{[i  |  j]\}
By
Latex:
(Unfold  `poset\_sig`  0  THEN  Auto)
Home
Index