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 b1 being Element of the Lines of S st {p,q} on b1
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 b1 being Element of the Lines of S st {p,q} on b1 ; :: thesis: verum