Let a, b and c be given.

We will prove affine_line_R2 a b c ⊆ EuclidPlane.

Let p be given.

Assume Hp: p ∈ affine_line_R2 a b c.

An exact proof term for the current goal is (SepE1 EuclidPlane (λp0 : set ⇒ add_SNo (mul_SNo a (R2_xcoord p0)) (mul_SNo b (R2_ycoord p0)) = c) p Hp).

∎