suffices L = Set.univ by rwa [← this]
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∀ (x y z : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, (∀ x ∈ L, x ∈ a') → L = a'
⊢ Set.univ.IsLine
case intro.intro
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : ∀ (x y z : V), ¬NotCollinear x y z
S : Set (Set V) := setOf Set.IsLine
this : S.Nonempty
L : Set V
hL : L ∈ S
hL' : ∀ a' ∈ S, (∀ x ∈ L, x ∈ a') → L = a'
⊢ L = Set.univ