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;
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 A1, A2, A7, A8, A6, INCPROJ:def 4;
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