for G being IncProjStr holds
( G is IncProjSp iff ( G is configuration & ( for p, q being POINT of G ex P being LINE of G st {p,q} on P ) & ex p being POINT of G ex P being LINE of G st p |' P & ( 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 ) ) & ( for a, b, c, d, p being POINT of G
for M, N, P, Q being LINE of G st {a,b,p} on M & {c,d,p} on N & {a,c} on P & {b,d} on Q & p |' P & p |' Q & M <> N holds
ex q being POINT of G st q on P,Q ) ) )