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 A1, Th8;

A5: a <> c by A4, ZFMISC_1:def 5;

A6: c on A by A3, INCSP_1:1;

A7: b <> c by A4, ZFMISC_1:def 5;

A8: b on A by A3, INCSP_1:1;

A9: a <> b by A4, ZFMISC_1:def 5;

( b on A & b |' B & a <> b ) ; :: thesis: verum

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 A1, Th8;

A5: a <> c by A4, ZFMISC_1:def 5;

A6: c on A by A3, INCSP_1:1;

A7: b <> c by A4, ZFMISC_1:def 5;

A8: b on A by A3, INCSP_1:1;

A9: a <> b by A4, ZFMISC_1:def 5;

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 ) ) )

hence
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 ) ) )

end;

( b on A & b |' B & a <> b ) ; :: thesis: verum