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

hereby :: thesis: ( G is configuration & ( for p, q being POINT of G ex M being LINE of G st {p,q} on M ) & ( for P, Q being LINE of G ex a being POINT of G st a on P,Q ) & ex a, b, c, d being POINT of G 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 G ex M being LINE of G st {p,q} on M ) & ( for P, Q being LINE of G ex a being POINT of G st a on P,Q ) & ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle )

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

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

thus for P, Q being LINE of G ex a being POINT of G st a on P,Q :: thesis: ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle

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

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

thus for P, Q being LINE of G ex a being POINT of G st a on P,Q :: thesis: ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle

proof

thus
ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle
by A1, Th15; :: thesis: verum
let P, Q be LINE of G; :: thesis: ex a being POINT of G st a on P,Q

consider a being POINT of G such that

A2: ( a on P & a on Q ) by A1, INCPROJ:def 9;

take a ; :: thesis: a on P,Q

thus a on P,Q by A2; :: thesis: verum

end;consider a being POINT of G such that

A2: ( a on P & a on Q ) by A1, INCPROJ:def 9;

take a ; :: thesis: a on P,Q

thus a on P,Q by A2; :: thesis: verum

hereby :: thesis: verum

assume that

A3: G is configuration and

A4: for p, q being POINT of G ex M being LINE of G st {p,q} on M and

A5: for P, Q being LINE of G ex a being POINT of G st a on P,Q and

A6: ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle ; :: thesis: G is IncProjectivePlane

ex a, b, c being POINT of G st a,b,c is_a_triangle by A6;

then A7: ex p being POINT of G ex P being LINE of G st p |' P by A4, Th17;

( ( 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 ) ) by A3, A4, A5, A6, Th22;

then reconsider G9 = G as IncProjSp by A3, A4, A7, Th4;

for P, Q being LINE of G9 ex a being POINT of G9 st

( a on P & a on Q )

end;A3: G is configuration and

A4: for p, q being POINT of G ex M being LINE of G st {p,q} on M and

A5: for P, Q being LINE of G ex a being POINT of G st a on P,Q and

A6: ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle ; :: thesis: G is IncProjectivePlane

ex a, b, c being POINT of G st a,b,c is_a_triangle by A6;

then A7: ex p being POINT of G ex P being LINE of G st p |' P by A4, Th17;

( ( 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 ) ) by A3, A4, A5, A6, Th22;

then reconsider G9 = G as IncProjSp by A3, A4, A7, Th4;

for P, Q being LINE of G9 ex a being POINT of G9 st

( a on P & a on Q )

proof

hence
G is IncProjectivePlane
by INCPROJ:def 9; :: thesis: verum
let P, Q be LINE of G9; :: thesis: ex a being POINT of G9 st

( a on P & a on Q )

consider a being POINT of G9 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; :: thesis: verum

end;( a on P & a on Q )

consider a being POINT of G9 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; :: thesis: verum