let G be IncProjStr ; :: thesis: ( G is IncProjSp implies ex A, B being LINE of G st A <> B )
assume A1: G is IncProjSp ; :: thesis: ex A, B being LINE of G st A <> B
consider a being POINT of G;
consider A, B, C being LINE of G such that
A2: ( a on A & a on B & a on C & A <> B & B <> C & C <> A ) by A1, PROJRED1:5;
take A ; :: thesis: ex B being LINE of G st A <> B
take B ; :: thesis: A <> B
thus A <> B by A2; :: thesis: verum