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 on P,Q & q on P,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 on P,Q & q on P,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 on P,Q & q on P,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 & q on P,Q & not p = q holds
P = Q
let P, Q be LINE of G; :: thesis: ( p on P,Q & q on P,Q & not p = q implies P = Q )
assume A2: ( p on P,Q & q on P,Q ) ; :: thesis: ( p = q or P = Q )
then A3: ( p on Q & q on Q ) by Def2;
( p on P & q on P ) by A2, Def2;
hence ( p = q or P = Q ) by A1, A3, Def4; :: thesis: verum

end;

hereby :: thesis: verum

assume A4: for p, q being POINT of G
for P, Q being LINE of G st p on P,Q & q on P,Q & not p = q holds
P = Q ; :: thesis: G is configuration

now

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 on P,Q & q on P,Q ) by Def2;
hence ( p = q or P = Q ) by A4; :: thesis: verum

end;

hence G is configuration by Def4; :: thesis: verum

end;