let G be IncProjStr ; :: thesis: ( G is IncProjectivePlane iff ( G is configuration & ( for p, q being POINT of ex M being LINE of st {p,q} on M ) & ( for P, Q being LINE of ex a being POINT of st a on P,Q ) & ex a, b, c, d being POINT of st a,b,c,d is_a_quadrangle ) )

hereby :: thesis: ( G is configuration & ( for p, q being POINT of ex M being LINE of st {p,q} on M ) & ( for P, Q being LINE of ex a being POINT of st a on P,Q ) & ex a, b, c, d being POINT of st a,b,c,d is_a_quadrangle implies G is IncProjectivePlane )

assume A1: G is IncProjectivePlane ; :: thesis: ( G is configuration & ( for p, q being POINT of ex M being LINE of st {p,q} on M ) & ( for P, Q being LINE of ex a being POINT of st a on P,Q ) & ex a, b, c, d being POINT of st a,b,c,d is_a_quadrangle )
hence G is configuration by Th4; :: thesis: ( ( for p, q being POINT of ex M being LINE of st {p,q} on M ) & ( for P, Q being LINE of ex a being POINT of st a on P,Q ) & ex a, b, c, d being POINT of st a,b,c,d is_a_quadrangle )
thus for p, q being POINT of ex M being LINE of st {p,q} on M by A1, Th4; :: thesis: ( ( for P, Q being LINE of ex a being POINT of st a on P,Q ) & ex a, b, c, d being POINT of st a,b,c,d is_a_quadrangle )
thus for P, Q being LINE of ex a being POINT of st a on P,Q :: thesis: ex a, b, c, d being POINT of st a,b,c,d is_a_quadrangle

proof

let P, Q be LINE of ; :: thesis: ex a being POINT of st a on P,Q
consider a being POINT of such that
A2: ( a on P & a on Q ) by A1, INCPROJ:def 14;
take a ; :: thesis: a on P,Q
thus a on P,Q by A2, Def2; :: thesis: verum

end;

thus ex a, b, c, d being POINT of st a,b,c,d is_a_quadrangle by A1, Th15; :: thesis: verum

end;

hereby :: thesis: verum

assume that
A3: G is configuration and
A4: for p, q being POINT of ex M being LINE of st {p,q} on M and
A5: for P, Q being LINE of ex a being POINT of st a on P,Q and
A6: ex a, b, c, d being POINT of st a,b,c,d is_a_quadrangle ; :: thesis: G is IncProjectivePlane
ex a, b, c being POINT of st a,b,c is_a_triangle by A6, Th18;
then A7: ex p being POINT of ex P being LINE of st p |' P by A4, Th17;
( ( for P being LINE of ex a, b, c being POINT of st
( a,b,c are_mutually_different & {a,b,c} on P ) ) & ( for a, b, c, d, p being POINT of
for M, N, P, Q being LINE of 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 st q on P,Q ) ) by A3, A4, A5, A6, Th22;
then reconsider G' = G as IncProjSp by A3, A4, A7, Th4;
for P, Q being LINE of ex a being POINT of st
( a on P & a on Q )

proof

let P, Q be LINE of ; :: thesis: ex a being POINT of st
( a on P & a on Q )
consider a being POINT of such that
A8: a on P,Q by A5;
take a ; :: thesis: ( a on P & a on Q )
thus ( a on P & a on Q ) by A8, Def2; :: thesis: verum

end;

hence G is IncProjectivePlane by INCPROJ:def 14; :: thesis: verum

end;