let G be IncProjStr ; :: thesis: for a being POINT of
for A being LINE of st G is IncProjSp holds
ex b, c being POINT of st
( {b,c} on A & a,b,c are_mutually_different )
let a be POINT of ; :: thesis: for A being LINE of st G is IncProjSp holds
ex b, c being POINT of st
( {b,c} on A & a,b,c are_mutually_different )
let A be LINE of ; :: thesis: ( G is IncProjSp implies ex b, c being POINT of st
( {b,c} on A & a,b,c are_mutually_different ) )
assume A1: G is IncProjSp ; :: thesis: ex b, c being POINT of st
( {b,c} on A & a,b,c are_mutually_different )
then consider b being POINT of such that
A2: ( b on A & b <> a ) and
b <> a by PROJRED1:8;
consider c being POINT of such that
A3: ( c on A & c <> a & c <> b ) by A1, PROJRED1:8;
take b ; :: thesis: ex c being POINT of st
( {b,c} on A & a,b,c are_mutually_different )
take c ; :: thesis: ( {b,c} on A & a,b,c are_mutually_different )
thus ( {b,c} on A & a,b,c are_mutually_different ) by A2, A3, INCSP_1:11, ZFMISC_1:def 5; :: thesis: verum