ordConnected_C2

lemma ordConnected_C2 : OrdConnected (ℭ₂ k n j : Set (𝔓 X)) := by  rw [ordConnected_def]; intro p mp p'' mp'' p' mp'  have mp₁ := mem_of_mem_of_subset mp ℭ₂_subset_ℭ₁  have mp'₁ : p' ∈ ℭ₁ (X := X) k n j := mem_of_mem_of_subset mp'    (ordConnected_C1.out mp₁ (mem_of_mem_of_subset mp'' ℭ₂_subset_ℭ₁))  by_cases e : p = p'; · rwa [e] at mp  simp_rw [ℭ₂, layersAbove, mem_sdiff, mp'₁, true_and]  by_contra h; rw [mem_iUnion₂] at h; obtain ⟨l', bl', p'm⟩ := h  rw [minLayer, mem_setOf, minimal_iff] at p'm  have pnm : p ∉ ⋃ l'', ⋃ (_ : l'' < l'), 𝔏₁ k n j l'' := by    replace mp := mp.2; contrapose! mp    exact mem_of_mem_of_subset mp      (iUnion_mono'' fun i ↦ iUnion_subset_iUnion_const fun hi ↦ (hi.trans_le bl').le)  exact absurd (p'm.2 ⟨mp.1, pnm⟩ mp'.1).symm e