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 on H & 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 on H & 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 on H & 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 A1: ( x1 on I & x2 on I & e on H & e |' I & x1 <> x2 & p1 <> e & p2 <> e & p1 on e * x1 & 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;
consider r being POINT of G such that
A2: ( r on p1 * p2 & r on H ) by INCPROJ:def 14;
A3: ( e on e * x1 & e on e * x2 & x1 on e * x1 & x2 on e * x2 ) by A1, Th16;
then A4: e * x1 <> e * x2 by A1, INCPROJ:def 9;
then p1 <> p2 by A1, A3, INCPROJ:def 9;
then A5: ( p1 on p1 * p2 & p2 on p1 * p2 ) by Th16;
then p1 * p2 <> e * x1 by A1, A3, A4, INCPROJ:def 9;
then r <> e by A1, A2, A3, A5, INCPROJ:def 9;
hence ex r being POINT of G st
( r on p1 * p2 & r on H & r <> e ) by A2; :: thesis: verum