let G be IncProjStr ; :: thesis: ( 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 )

for P, Q being LINE of G st {p,q} on P & {p,q} on Q & not p = q holds

P = Q )

hereby :: thesis: ( ( 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 )

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
; :: thesis: 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

let p, q be POINT of G; :: thesis: for P, Q being LINE of G st {p,q} on P & {p,q} on Q & not p = q holds

P = Q

let P, Q be LINE of G; :: thesis: ( {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 ; :: thesis: ( 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; :: thesis: verum

end;for P, Q being LINE of G st {p,q} on P & {p,q} on Q & not p = q holds

P = Q

let p, q be POINT of G; :: thesis: for P, Q being LINE of G st {p,q} on P & {p,q} on Q & not p = q holds

P = Q

let P, Q be LINE of G; :: thesis: ( {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 ; :: thesis: ( 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; :: thesis: verum

hereby :: thesis: 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 ; :: thesis: G is configuration

end;for P, Q being LINE of G st {p,q} on P & {p,q} on Q & not p = q holds

P = Q ; :: thesis: G is configuration

now :: thesis: 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 = Q

hence
G is configuration
; :: thesis: verumfor P, Q being LINE of G st p on P & q on P & p on Q & q on Q & not p = q holds

P = Q

let p, q be POINT of G; :: thesis: 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 = Q

let P, Q be LINE of G; :: thesis: ( 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 ) ; :: thesis: ( 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; :: thesis: verum

end;P = Q

let P, Q be LINE of G; :: thesis: ( 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 ) ; :: thesis: ( 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; :: thesis: verum