hereby :: thesis: ( ( for p, q being POINT of S ex P being LINE of S st
( p on P & q on P ) ) implies S is linear )

assume A1: S is linear ; :: thesis: for p, q being POINT of S ex P being LINE of S st
( p on P & q on P )
let p, q be POINT of S; :: thesis: ex P being LINE of S st
( p on P & q on P )
consider P being LINE of S such that
A2: {p,q} on P by A1;
take P = P; :: thesis: ( p on P & q on P )
thus ( p on P & q on P ) by A2, INCSP_1:1; :: thesis: verum

end;

assume A3: for p, q being POINT of S ex P being LINE of S st
( p on P & q on P ) ; :: thesis: S is linear
let p, q be POINT of S; :: according to INCSP_1:def 9 :: thesis: ex b₁ being Element of the Lines of S st {p,q} on b₁
consider L being LINE of S such that
A4: ( p on L & q on L ) by A3;
{p,q} on L by A4, INCSP_1:1;
hence ex b₁ being Element of the Lines of S st {p,q} on b₁ ; :: thesis: verum