Step * of Lemma subinterval_transitivity

[I,J,K:Interval].  (I ⊆ J   J ⊆ K   I ⊆ )
BY
(Unfold `subinterval` THEN Auto) }


Latex:


Latex:
\mforall{}[I,J,K:Interval].    (I  \msubseteq{}  J    {}\mRightarrow{}  J  \msubseteq{}  K    {}\mRightarrow{}  I  \msubseteq{}  K  )


By


Latex:
(Unfold  `subinterval`  0  THEN  Auto)




Home Index