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 ) ) )

( 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 )

( 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 ) )

( 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

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

end;( 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

thus
ex p being POINT of G ex P being LINE of G st p |' P
by A1, INCPROJ:def 6; :: thesis: ( ( for P being LINE of G ex a, b, c being POINT of G st
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 A1, INCPROJ:def 5;

take P ; :: thesis: {p,q} on P

thus {p,q} on P by A2, INCSP_1:1; :: thesis: verum

end;consider P being LINE of G such that

A2: ( p on P & q on P ) by A1, INCPROJ:def 5;

take P ; :: thesis: {p,q} on P

thus {p,q} on P by A2, INCSP_1:1; :: thesis: verum

( 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

thus
for a, b, c, d, p being POINT of G
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 A1, INCPROJ:def 7;

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 A3, ZFMISC_1:def 5; :: thesis: {a,b,c} on P

thus {a,b,c} on P by A4, INCSP_1:2; :: thesis: verum

end;( 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 A1, INCPROJ:def 7;

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 A3, ZFMISC_1:def 5; :: thesis: {a,b,c} on P

thus {a,b,c} on P by A4, INCSP_1:2; :: thesis: verum

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 A5, INCSP_1:2;

A11: ( a on P & c on P ) by A7, INCSP_1:1;

A12: ( d on N & p on N ) by A6, INCSP_1:2;

A13: ( b on Q & d on Q ) by A8, INCSP_1:1;

( p on M & c on N ) by A5, A6, INCSP_1:2;

then consider q being POINT of G such that

A14: ( q on P & q on Q ) by A1, A9, A10, A12, A11, A13, INCPROJ:def 8;

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

thus q on P,Q by A14; :: thesis: verum

end;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 A5, INCSP_1:2;

A11: ( a on P & c on P ) by A7, INCSP_1:1;

A12: ( d on N & p on N ) by A6, INCSP_1:2;

A13: ( b on Q & d on Q ) by A8, INCSP_1:1;

( p on M & c on N ) by A5, A6, INCSP_1:2;

then consider q being POINT of G such that

A14: ( q on P & q on Q ) by A1, A9, A10, A12, A11, A13, INCPROJ:def 8;

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

thus q on P,Q by A14; :: thesis: verum

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

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 )

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 A17, A20, A22, A27, INCPROJ:def 4, INCPROJ:def 5, INCPROJ:def 6, INCPROJ:def 7, INCPROJ:def 8; :: thesis: verum

end;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 )

( 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 A21, INCSP_1:1; :: thesis: verum

end;( 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 A21, INCSP_1:1; :: thesis: verum

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 )

A27:
for a, b, c, d, p, q being POINT of G( 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 A23, ZFMISC_1:def 5;

A26: ( b on P & c on P ) by A24, INCSP_1:2;

( c <> a & a on P ) by A23, A24, INCSP_1:2, ZFMISC_1:def 5;

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 A25, A26; :: thesis: verum

end;( 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 A23, ZFMISC_1:def 5;

A26: ( b on P & c on P ) by A24, INCSP_1:2;

( c <> a & a on P ) by A23, A24, INCSP_1:2, ZFMISC_1:def 5;

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 A25, A26; :: thesis: verum

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

for p, q being POINT of G
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 A29, INCSP_1:1;

( {a,b,p} on M & {c,d,p} on N ) by A28, INCSP_1:2;

then consider q1 being POINT of G such that

A32: q1 on P,Q by A19, A30, A31;

take q1 ; :: thesis: ( q1 on P & q1 on Q )

thus ( q1 on P & q1 on Q ) by A32; :: thesis: verum

end;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 A29, INCSP_1:1;

( {a,b,p} on M & {c,d,p} on N ) by A28, INCSP_1:2;

then consider q1 being POINT of G such that

A32: q1 on P,Q by A19, A30, A31;

take q1 ; :: thesis: ( q1 on P & q1 on Q )

thus ( q1 on P & q1 on Q ) by A32; :: thesis: verum

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 A17, A20, A22, A27, INCPROJ:def 4, INCPROJ:def 5, INCPROJ:def 6, INCPROJ:def 7, INCPROJ:def 8; :: thesis: verum