let G be IncProjectivePlane; 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; 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; ( 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
; ( (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; (q * a) * B |' A
assume A9:
(q * a) * B on A
; contradiction
(q * a) * B on q * a
by A8, Th24;
then
a = (q * a) * B
by A2, A3, A6, A9, A5;
hence
contradiction
by A7, A8, Th24; verum