let G be IncProjStr ; :: thesis: ( G is IncProjSp iff ( G is configuration & ( for p, q being POINT of G ex P being LINE of G st {p,q} on P ) & ex p being POINT of G ex P being LINE of G st p |' P & ( 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 ) ) )

hereby :: thesis: ( G is configuration & ( for p, q being POINT of G ex P being LINE of G st {p,q} on P ) & ex p being POINT of G ex P being LINE of G st p |' P & ( 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 ) implies G is IncProjSp )
assume A1: G is IncProjSp ; :: thesis: ( G is configuration & ( for p, q being POINT of G ex P being LINE of G st {p,q} on P ) & ex p being POINT of G ex P being LINE of G st p |' P & ( 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 ) )

then 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 by INCPROJ:def 4;
hence G is configuration ; :: thesis: ( ( for p, q being POINT of G ex P being LINE of G st {p,q} on P ) & ex p being POINT of G ex P being LINE of G st p |' P & ( 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 ) )

thus for p, q being POINT of G ex P being LINE of G st {p,q} on P :: thesis: ( ex p being POINT of G ex P being LINE of G st p |' P & ( 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 ) )
proof
let p, q be POINT of G; :: thesis: ex P being LINE of G st {p,q} on P
consider P being LINE of G such that
A2: ( p on P & q on P ) by ;
take P ; :: thesis: {p,q} on P
thus {p,q} on P by ; :: thesis: verum
end;
thus ex p being POINT of G ex P being LINE of G st p |' P by ; :: thesis: ( ( 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 ) )

thus 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 ) :: thesis: 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
proof
let P be LINE of G; :: thesis: ex a, b, c being POINT of G st
( a,b,c are_mutually_distinct & {a,b,c} on P )

consider a, b, c being POINT of G such that
A3: ( a <> b & b <> c & c <> a ) and
A4: ( a on P & b on P & c on P ) by ;
take a ; :: thesis: ex b, c being POINT of G st
( a,b,c are_mutually_distinct & {a,b,c} on P )

take b ; :: thesis: ex c being POINT of G st
( a,b,c are_mutually_distinct & {a,b,c} on P )

take c ; :: thesis: ( a,b,c are_mutually_distinct & {a,b,c} on P )
thus a,b,c are_mutually_distinct by ; :: thesis: {a,b,c} on P
thus {a,b,c} on P by ; :: thesis: verum
end;
thus 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 :: thesis: verum
proof
let a, b, c, d, p be POINT of G; :: thesis: 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

let M, N, P, Q be LINE of G; :: thesis: ( {a,b,p} on M & {c,d,p} on N & {a,c} on P & {b,d} on Q & p |' P & p |' Q & M <> N implies ex q being POINT of G st q on P,Q )
assume that
A5: {a,b,p} on M and
A6: {c,d,p} on N and
A7: {a,c} on P and
A8: {b,d} on Q and
A9: ( p |' P & p |' Q & M <> N ) ; :: thesis: ex q being POINT of G st q on P,Q
A10: ( a on M & b on M ) by ;
A11: ( a on P & c on P ) by ;
A12: ( d on N & p on N ) by ;
A13: ( b on Q & d on Q ) by ;
( p on M & c on N ) by ;
then consider q being POINT of G such that
A14: ( q on P & q on Q ) by ;
take q ; :: thesis: q on P,Q
thus q on P,Q by A14; :: thesis: verum
end;
end;
hereby :: thesis: verum
assume that
A15: G is configuration and
A16: for p, q being POINT of G ex P being LINE of G st {p,q} on P and
A17: ex p being POINT of G ex P being LINE of G st p |' P and
A18: 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 ) and
A19: 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 ; :: thesis: G is IncProjSp
A20: now :: thesis: for p, q being POINT of G ex P being LINE of G st
( p on P & q on P )
let p, q be POINT of G; :: thesis: ex P being LINE of G st
( p on P & q on P )

consider P being LINE of G such that
A21: {p,q} on P by A16;
take P = P; :: thesis: ( p on P & q on P )
thus ( p on P & q on P ) by ; :: thesis: verum
end;
A22: now :: thesis: for P being LINE of G ex a, b, c being POINT of G st
( a <> b & b <> c & c <> a & a on P & b on P & c on P )
let P be LINE of G; :: thesis: ex a, b, c being POINT of G st
( a <> b & b <> c & c <> a & a on P & b on P & c on P )

consider a, b, c being POINT of G such that
A23: a,b,c are_mutually_distinct and
A24: {a,b,c} on P by A18;
A25: ( a <> b & b <> c ) by ;
A26: ( b on P & c on P ) by ;
( c <> a & a on P ) by ;
hence ex a, b, c being POINT of G st
( a <> b & b <> c & c <> a & a on P & b on P & c on P ) by ; :: thesis: verum
end;
A27: for a, b, c, d, p, q being POINT of G
for M, N, P, Q being LINE of G st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being POINT of G st
( q on P & q on Q )
proof
let a, b, c, d, p, q be POINT of G; :: thesis: for M, N, P, Q being LINE of G st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being POINT of G st
( q on P & q on Q )

let M, N, P, Q be LINE of G; :: thesis: ( a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N implies ex q being POINT of G st
( q on P & q on Q ) )

assume that
A28: ( a on M & b on M & c on N & d on N & p on M & p on N ) and
A29: ( a on P & c on P & b on Q & d on Q ) and
A30: ( not p on P & not p on Q & M <> N ) ; :: thesis: ex q being POINT of G st
( q on P & q on Q )

A31: ( {a,c} on P & {b,d} on Q ) by ;
( {a,b,p} on M & {c,d,p} on N ) by ;
then consider q1 being POINT of G such that
A32: q1 on P,Q by ;
take q1 ; :: thesis: ( q1 on P & q1 on Q )
thus ( q1 on P & q1 on Q ) by A32; :: thesis: verum
end;
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 by A15;
hence G is IncProjSp by ; :: thesis: verum
end;