consider P, Q being Point of real_projective_plane such that
A1: P <> Q and
A2: l = Line (P,Q) by BKMODEL1:72;
L2P (P,Q) is Point of real_projective_plane ;
hence ex b₁, P, Q being Point of real_projective_plane st
( P <> Q & l = Line (P,Q) & b₁ = L2P (P,Q) ) by A1, A2; :: thesis: verum