English
If G is IsFiveWheelLike with parameters r,k and there is a single-vertex x adjacent to all vertices in a large set except at most two, then there exists a FiveWheelLike with parameters r,k+1 after inserting x and adjusting the relevant sets.
Русский
Если G имеет структуру IsFiveWheelLike с параметрами r,k и существует вершина x, соседняя со всеми вершинами в большой совокупности кроме как с двумя, то существует структура FiveWheelLike с параметрами r, k+1 после вставки x и корректировки соответствующих множеств.
LaTeX
$$$$ \\exists a,b:\\; G.IsFiveWheelLike r (k+1) v w_1 w_2 (\\mathrm{insert}\\; x \\; (s \\setminus \\{a\\})) (\\mathrm{insert}\\; x \\; (t \\setminus \\{b\\})). $$$$
Lean4
@[symm]
theorem symm : G.IsFiveWheelLike r k v w₂ w₁ t s :=
let ⟨p2, d1, d2, d3, d4, c1, c2, c3, c4, hk⟩ := hw
⟨p2.symm, d2, d1, d4, d3, c3, c4, c1, c2, by rwa [inter_comm]⟩
