let G be IncProjectivePlane; 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; 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; ( 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
; 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; verum