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
proof
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;
thus ex a, b, c, d being POINT of G 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 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
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;
hence G is IncProjectivePlane by INCPROJ:def 9; :: thesis: verum
end;