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 A1, INCPROJ:def 5;
take P ; :: thesis: {p,q} on P
thus {p,q} on P by A2, INCSP_1:1; :: thesis: verum
end;
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
( 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 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;
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 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;
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 A21, INCSP_1:1; :: 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 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;
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 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;
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 A17, A20, A22, A27, INCPROJ:def 4, INCPROJ:def 5, INCPROJ:def 6, INCPROJ:def 7, INCPROJ:def 8; :: thesis: verum
end;