let G be IncProjStr ; :: thesis: ( G is IncProjSp implies ex A, B being LINE of G st A <> B )
set a = the 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
the POINT of G on A and
the POINT of G on B and
the POINT of G 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