let G be IncProjStr ; :: thesis: for a, p, q, r being POINT of G
for A, P, Q, R being LINE of G st G is configuration & a on P,Q,R & P,Q,R are_mutually_distinct & a |' A & p on A,P & q on A,Q & r on A,R holds
p,q,r are_mutually_distinct

let a, p, q, r be POINT of G; :: thesis: for A, P, Q, R being LINE of G st G is configuration & a on P,Q,R & P,Q,R are_mutually_distinct & a |' A & p on A,P & q on A,Q & r on A,R holds
p,q,r are_mutually_distinct

let A, P, Q, R be LINE of G; :: thesis: ( G is configuration & a on P,Q,R & P,Q,R are_mutually_distinct & a |' A & p on A,P & q on A,Q & r on A,R implies p,q,r are_mutually_distinct )
assume that
A1: G is configuration and
A2: a on P,Q,R and
A3: P,Q,R are_mutually_distinct and
A4: a |' A and
A5: p on A,P and
A6: q on A,Q and
A7: r on A,R ; :: thesis:
A8: ( a on R & r on R ) by A2, A7;
A9: ( a on Q & q on Q ) by A2, A6;
( Q <> R & q on A ) by ;
then A10: q <> r by A1, A4, A9, A8;
A11: p on P by A5;
A12: ( a on P & p on A ) by A2, A5;
R <> P by ;
then A13: r <> p by A1, A4, A12, A11, A8;
P <> Q by ;
then p <> q by A1, A4, A12, A11, A9;
hence p,q,r are_mutually_distinct by ; :: thesis: verum