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

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