theorem EuclidGeom.Parallel.segnd_para_line_of_line_para_line {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (B_ne_A : B ≠ A) (l : EuclidGeom.Line P) (h : EuclidGeom.Parallel (SEG_nd A B B_ne_A) l) : EuclidGeom.Parallel (LIN A B B_ne_A) l