Theorem: Fano.Fano.point_line_uniq (ProjectivePlane.lean)

State before:
P L : Type
⊢ ∀ {p q : Points} {l m : Lines}, p ∈ l → q ∈ l → p ∈ m → q ∈ m → p = q ∨ l = m
Tactic:
decide
State after:
no goals