let G be IncProjectivePlane; :: thesis: for a, q being POINT of G
for A, B being LINE of G st A <> B & a on A & q |' A & a <> A * B holds
( (q * a) * B on B & (q * a) * B |' A )

let a, q be POINT of G; :: thesis: for A, B being LINE of G st A <> B & a on A & q |' A & a <> A * B holds
( (q * a) * B on B & (q * a) * B |' A )

let A, B be LINE of G; :: thesis: ( A <> B & a on A & q |' A & a <> A * B implies ( (q * a) * B on B & (q * a) * B |' A ) )
assume that
A1: A <> B and
A2: a on A and
A3: q |' A and
A4: a <> A * B ; :: thesis: ( (q * a) * B on B & (q * a) * B |' A )
set D = q * a;
A5: ( a on q * a & q on q * a ) by A2, A3, Th16;
set d = (q * a) * B;
A6: G is configuration by Th23;
A7: a |' B by A1, A2, A4, Th24;
then A8: q * a <> B by A2, A3, Th16;
hence (q * a) * B on B by Th24; :: thesis: (q * a) * B |' A
assume A9: (q * a) * B on A ; :: thesis: contradiction
(q * a) * B on q * a by ;
then a = (q * a) * B by A2, A3, A6, A9, A5;
hence contradiction by A7, A8, Th24; :: thesis: verum