let G be IncProjStr ; :: thesis: for a being POINT of G
for A, B being LINE of G st G is IncProjSp & A <> B holds
ex b being POINT of G st
( b on A & b |' B & a <> b )

let a be POINT of G; :: thesis: for A, B being LINE of G st G is IncProjSp & A <> B holds
ex b being POINT of G st
( b on A & b |' B & a <> b )

let A, B be LINE of G; :: thesis: ( G is IncProjSp & A <> B implies ex b being POINT of G st
( b on A & b |' B & a <> b ) )

assume that
A1: G is IncProjSp and
A2: A <> B ; :: thesis: ex b being POINT of G st
( b on A & b |' B & a <> b )

consider b, c being POINT of G such that
A3: {b,c} on A and
A4: a,b,c are_mutually_distinct by ;
A5: a <> c by ;
A6: c on A by ;
A7: b <> c by ;
A8: b on A by ;
A9: a <> b by ;
now :: thesis: ( ( b |' B & ex b being POINT of G st
( b on A & b |' B & a <> b ) ) or ( c |' B & ex b being POINT of G st
( b on A & b |' B & a <> b ) ) )
per cases ( b |' B or c |' B ) by ;
case b |' B ; :: thesis: ex b being POINT of G st
( b on A & b |' B & a <> b )

hence ex b being POINT of G st
( b on A & b |' B & a <> b ) by A9, A8; :: thesis: verum
end;
case c |' B ; :: thesis: ex b being POINT of G st
( b on A & b |' B & a <> b )

hence ex b being POINT of G st
( b on A & b |' B & a <> b ) by A5, A6; :: thesis: verum
end;
end;
end;
hence ex b being POINT of G st
( b on A & b |' B & a <> b ) ; :: thesis: verum