Transitions on closed fragments

Closed fragments have no boundary labels, so every flag attaches internally, and every Eulerian edge subset admits an oriented transition system: the choice in the Definition 5 value is always inhabited.

theorem RS.ClosedFragment.attach_internal (W : ClosedFragment) (f : W.Flag) : ∃ (v : W.Vertex), W.attach f = Sum.inl v

Every flag of a closed fragment attaches to a vertex.

theorem RS.ClosedFragment.eulerian_transition_nonempty (W : ClosedFragment) (F : EdgeSubset W) (hE : F.Eulerian) : Nonempty ((κ : F.TransitionSystem) × κ.Orientation)

Eulerian subsets of closed fragments admit oriented transition systems.