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 A8, Th24;

then a = (q * a) * B by A2, A3, A6, A9, A5;

hence contradiction by A7, A8, Th24; :: thesis: verum

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 A8, Th24;

then a = (q * a) * B by A2, A3, A6, A9, A5;

hence contradiction by A7, A8, Th24; :: thesis: verum