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