let G be IncProjectivePlane; :: thesis: for e, x1, x2, p1, p2 being POINT of G

for H, I being LINE of G st x1 on I & x2 on I & e |' I & x1 <> x2 & p1 <> e & p2 <> e & p1 on e * x1 & p2 on e * x2 holds

ex r being POINT of G st

( r on p1 * p2 & r on H & r <> e )

let e, x1, x2, p1, p2 be POINT of G; :: thesis: for H, I being LINE of G st x1 on I & x2 on I & e |' I & x1 <> x2 & p1 <> e & p2 <> e & p1 on e * x1 & p2 on e * x2 holds

ex r being POINT of G st

( r on p1 * p2 & r on H & r <> e )

let H, I be LINE of G; :: thesis: ( x1 on I & x2 on I & e |' I & x1 <> x2 & p1 <> e & p2 <> e & p1 on e * x1 & p2 on e * x2 implies ex r being POINT of G st

( r on p1 * p2 & r on H & r <> e ) )

assume that

A1: x1 on I and

A2: x2 on I and

A3: e |' I and

A4: x1 <> x2 and

A5: p1 <> e and

A6: p2 <> e and

A7: p1 on e * x1 and

A8: p2 on e * x2 ; :: thesis: ex r being POINT of G st

( r on p1 * p2 & r on H & r <> e )

set L1 = e * x1;

set L2 = e * x2;

set L = p1 * p2;

A9: e on e * x1 by A1, A3, Th16;

A10: e on e * x2 by A2, A3, Th16;

( x1 on e * x1 & x2 on e * x2 ) by A1, A2, A3, Th16;

then A11: e * x1 <> e * x2 by A1, A2, A3, A4, A9, INCPROJ:def 4;

then A12: p1 <> p2 by A5, A7, A8, A9, A10, INCPROJ:def 4;

then p2 on p1 * p2 by Th16;

then A13: p1 * p2 <> e * x1 by A6, A8, A9, A10, A11, INCPROJ:def 4;

consider r being POINT of G such that

A14: r on p1 * p2 and

A15: r on H by INCPROJ:def 9;

p1 on p1 * p2 by A12, Th16;

then r <> e by A5, A7, A14, A9, A13, INCPROJ:def 4;

hence ex r being POINT of G st

( r on p1 * p2 & r on H & r <> e ) by A14, A15; :: thesis: verum

for H, I being LINE of G st x1 on I & x2 on I & e |' I & x1 <> x2 & p1 <> e & p2 <> e & p1 on e * x1 & p2 on e * x2 holds

ex r being POINT of G st

( r on p1 * p2 & r on H & r <> e )

let e, x1, x2, p1, p2 be POINT of G; :: thesis: for H, I being LINE of G st x1 on I & x2 on I & e |' I & x1 <> x2 & p1 <> e & p2 <> e & p1 on e * x1 & p2 on e * x2 holds

ex r being POINT of G st

( r on p1 * p2 & r on H & r <> e )

let H, I be LINE of G; :: thesis: ( x1 on I & x2 on I & e |' I & x1 <> x2 & p1 <> e & p2 <> e & p1 on e * x1 & p2 on e * x2 implies ex r being POINT of G st

( r on p1 * p2 & r on H & r <> e ) )

assume that

A1: x1 on I and

A2: x2 on I and

A3: e |' I and

A4: x1 <> x2 and

A5: p1 <> e and

A6: p2 <> e and

A7: p1 on e * x1 and

A8: p2 on e * x2 ; :: thesis: ex r being POINT of G st

( r on p1 * p2 & r on H & r <> e )

set L1 = e * x1;

set L2 = e * x2;

set L = p1 * p2;

A9: e on e * x1 by A1, A3, Th16;

A10: e on e * x2 by A2, A3, Th16;

( x1 on e * x1 & x2 on e * x2 ) by A1, A2, A3, Th16;

then A11: e * x1 <> e * x2 by A1, A2, A3, A4, A9, INCPROJ:def 4;

then A12: p1 <> p2 by A5, A7, A8, A9, A10, INCPROJ:def 4;

then p2 on p1 * p2 by Th16;

then A13: p1 * p2 <> e * x1 by A6, A8, A9, A10, A11, INCPROJ:def 4;

consider r being POINT of G such that

A14: r on p1 * p2 and

A15: r on H by INCPROJ:def 9;

p1 on p1 * p2 by A12, Th16;

then r <> e by A5, A7, A14, A9, A13, INCPROJ:def 4;

hence ex r being POINT of G st

( r on p1 * p2 & r on H & r <> e ) by A14, A15; :: thesis: verum