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