let G be IncProjStr ; ( G is configuration iff for p, q being POINT of G
for P, Q being LINE of G st {p,q} on P & {p,q} on Q & not p = q holds
P = Q )
hereby ( ( for p, q being POINT of G
for P, Q being LINE of G st {p,q} on P & {p,q} on Q & not p = q holds
P = Q ) implies G is configuration )
assume A1:
G is
configuration
;
for p, q being POINT of G
for P, Q being LINE of G st {p,q} on P & {p,q} on Q & not p = q holds
P = Qlet p,
q be
POINT of
G;
for P, Q being LINE of G st {p,q} on P & {p,q} on Q & not p = q holds
P = Qlet P,
Q be
LINE of
G;
( {p,q} on P & {p,q} on Q & not p = q implies P = Q )assume that A2:
{p,q} on P
and A3:
{p,q} on Q
;
( p = q or P = Q )A4:
(
p on Q &
q on Q )
by A3, INCSP_1:1;
(
p on P &
q on P )
by A2, INCSP_1:1;
hence
(
p = q or
P = Q )
by A1, A4;
verum
end;
hereby verum
assume A5:
for
p,
q being
POINT of
G for
P,
Q being
LINE of
G st
{p,q} on P &
{p,q} on Q & not
p = q holds
P = Q
;
G is configuration now for p, q being POINT of G
for P, Q being LINE of G st p on P & q on P & p on Q & q on Q & not p = q holds
P = Qlet p,
q be
POINT of
G;
for P, Q being LINE of G st p on P & q on P & p on Q & q on Q & not p = q holds
P = Qlet P,
Q be
LINE of
G;
( p on P & q on P & p on Q & q on Q & not p = q implies P = Q )assume
(
p on P &
q on P &
p on Q &
q on Q )
;
( p = q or P = Q )then
(
{p,q} on P &
{p,q} on Q )
by INCSP_1:1;
hence
(
p = q or
P = Q )
by A5;
verum end; hence
G is
configuration
;
verum
end;