let G be IncProjStr ; :: thesis: for a being POINT of G

for A being LINE of G st G is IncProjSp holds

ex b, c being POINT of G st

( {b,c} on A & a,b,c are_mutually_distinct )

let a be POINT of G; :: thesis: for A being LINE of G st G is IncProjSp holds

ex b, c being POINT of G st

( {b,c} on A & a,b,c are_mutually_distinct )

let A be LINE of G; :: thesis: ( G is IncProjSp implies ex b, c being POINT of G st

( {b,c} on A & a,b,c are_mutually_distinct ) )

assume A1: G is IncProjSp ; :: thesis: ex b, c being POINT of G st

( {b,c} on A & a,b,c are_mutually_distinct )

then consider b being POINT of G such that

A2: ( b on A & b <> a ) and

b <> a by PROJRED1:8;

consider c being POINT of G such that

A3: ( c on A & c <> a & c <> b ) by A1, PROJRED1:8;

take b ; :: thesis: ex c being POINT of G st

( {b,c} on A & a,b,c are_mutually_distinct )

take c ; :: thesis: ( {b,c} on A & a,b,c are_mutually_distinct )

thus ( {b,c} on A & a,b,c are_mutually_distinct ) by A2, A3, INCSP_1:1, ZFMISC_1:def 5; :: thesis: verum

for A being LINE of G st G is IncProjSp holds

ex b, c being POINT of G st

( {b,c} on A & a,b,c are_mutually_distinct )

let a be POINT of G; :: thesis: for A being LINE of G st G is IncProjSp holds

ex b, c being POINT of G st

( {b,c} on A & a,b,c are_mutually_distinct )

let A be LINE of G; :: thesis: ( G is IncProjSp implies ex b, c being POINT of G st

( {b,c} on A & a,b,c are_mutually_distinct ) )

assume A1: G is IncProjSp ; :: thesis: ex b, c being POINT of G st

( {b,c} on A & a,b,c are_mutually_distinct )

then consider b being POINT of G such that

A2: ( b on A & b <> a ) and

b <> a by PROJRED1:8;

consider c being POINT of G such that

A3: ( c on A & c <> a & c <> b ) by A1, PROJRED1:8;

take b ; :: thesis: ex c being POINT of G st

( {b,c} on A & a,b,c are_mutually_distinct )

take c ; :: thesis: ( {b,c} on A & a,b,c are_mutually_distinct )

thus ( {b,c} on A & a,b,c are_mutually_distinct ) by A2, A3, INCSP_1:1, ZFMISC_1:def 5; :: thesis: verum