for G being IncProjStr
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