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 ;
then A12: p1 <> p2 by ;
then p2 on p1 * p2 by Th16;
then A13: p1 * p2 <> e * x1 by ;
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 ;
then r <> e by ;
hence ex r being POINT of G st
( r on p1 * p2 & r on H & r <> e ) by ; :: thesis: verum