theorem Th4:
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 ) ) )