for G being IncProjStr st G is configuration & ( for p, q being POINT of G ex M being LINE of G st {p,q} on M ) & ( for P, Q being LINE of G ex a being POINT of G st a on P,Q ) & ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle holds
for P being LINE of G ex a, b, c being POINT of G st
( a,b,c are_mutually_distinct & {a,b,c} on P )