let G be IncProjStr ; :: 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 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 ) )

assume that

A1: G is configuration and

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

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

A4: ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle ; :: 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 )

( a,b,c are_mutually_distinct & {a,b,c} on P ) )

assume that

A1: G is configuration and

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

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

A4: ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle ; :: 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 )

hereby :: thesis: verum

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, d being POINT of G such that

A5: a,b,c,d is_a_quadrangle by A4;

A6: a,b,c is_a_triangle by A5;

thus ex a, b, c being POINT of G st

( a,b,c are_mutually_distinct & {a,b,c} on P ) :: thesis: verum

end;( a,b,c are_mutually_distinct & {a,b,c} on P )

consider a, b, c, d being POINT of G such that

A5: a,b,c,d is_a_quadrangle by A4;

A6: a,b,c is_a_triangle by A5;

thus ex a, b, c being POINT of G st

( a,b,c are_mutually_distinct & {a,b,c} on P ) :: thesis: verum

proof

( a,b,c are_mutually_distinct & {a,b,c} on P ) ; :: thesis: verum

end;

now :: thesis: ( ( a |' P & ex a, b, c being POINT of G st

( a,b,c are_mutually_distinct & {a,b,c} on P ) ) or ( b |' P & ex a, b, c being POINT of G st

( a,b,c are_mutually_distinct & {a,b,c} on P ) ) or ( c |' P & ex a, b, c being POINT of G st

( a,b,c are_mutually_distinct & {a,b,c} on P ) ) )end;

hence
ex a, b, c being POINT of G st ( a,b,c are_mutually_distinct & {a,b,c} on P ) ) or ( b |' P & ex a, b, c being POINT of G st

( a,b,c are_mutually_distinct & {a,b,c} on P ) ) or ( c |' P & ex a, b, c being POINT of G st

( a,b,c are_mutually_distinct & {a,b,c} on P ) ) )

per cases
( a |' P or b |' P or c |' P )
by A6, Th5;

end;

case A7:
a |' P
; :: thesis: ex a, b, c being POINT of G st

( a,b,c are_mutually_distinct & {a,b,c} on P )

( a,b,c are_mutually_distinct & {a,b,c} on P )

consider B being LINE of G such that

A8: {a,b} on B by A2;

consider D being LINE of G such that

A9: {a,d} on D by A2;

consider C being LINE of G such that

A10: {a,c} on C by A2;

A11: a on D by A9, INCSP_1:1;

A12: a on C by A10, INCSP_1:1;

a on B by A8, INCSP_1:1;

then A13: a on B,C,D by A12, A11;

consider p being POINT of G such that

A14: p on P,B by A3;

A15: B,C,D are_mutually_distinct by A5, A8, A10, A9, Th20;

consider q being POINT of G such that

A16: q on P,C by A3;

A17: q on P by A16;

consider r being POINT of G such that

A18: r on P,D by A3;

A19: r on P by A18;

p on P by A14;

then {p,q,r} on P by A17, A19, INCSP_1:2;

hence ex a, b, c being POINT of G st

( a,b,c are_mutually_distinct & {a,b,c} on P ) by A1, A7, A13, A15, A14, A16, A18, Th21; :: thesis: verum

end;A8: {a,b} on B by A2;

consider D being LINE of G such that

A9: {a,d} on D by A2;

consider C being LINE of G such that

A10: {a,c} on C by A2;

A11: a on D by A9, INCSP_1:1;

A12: a on C by A10, INCSP_1:1;

a on B by A8, INCSP_1:1;

then A13: a on B,C,D by A12, A11;

consider p being POINT of G such that

A14: p on P,B by A3;

A15: B,C,D are_mutually_distinct by A5, A8, A10, A9, Th20;

consider q being POINT of G such that

A16: q on P,C by A3;

A17: q on P by A16;

consider r being POINT of G such that

A18: r on P,D by A3;

A19: r on P by A18;

p on P by A14;

then {p,q,r} on P by A17, A19, INCSP_1:2;

hence ex a, b, c being POINT of G st

( a,b,c are_mutually_distinct & {a,b,c} on P ) by A1, A7, A13, A15, A14, A16, A18, Th21; :: thesis: verum

case A20:
b |' P
; :: thesis: ex a, b, c being POINT of G st

( a,b,c are_mutually_distinct & {a,b,c} on P )

( a,b,c are_mutually_distinct & {a,b,c} on P )

consider B being LINE of G such that

A21: {b,a} on B by A2;

consider D being LINE of G such that

A22: {b,d} on D by A2;

consider C being LINE of G such that

A23: {b,c} on C by A2;

A24: b on D by A22, INCSP_1:1;

A25: b on C by A23, INCSP_1:1;

b on B by A21, INCSP_1:1;

then A26: b on B,C,D by A25, A24;

consider q being POINT of G such that

A27: q on P,C by A3;

b,a,c,d is_a_quadrangle by A5, Th13;

then A28: B,C,D are_mutually_distinct by A21, A23, A22, Th20;

consider p being POINT of G such that

A29: p on P,B by A3;

A30: q on P by A27;

consider r being POINT of G such that

A31: r on P,D by A3;

A32: r on P by A31;

p on P by A29;

then {p,q,r} on P by A30, A32, INCSP_1:2;

hence ex a, b, c being POINT of G st

( a,b,c are_mutually_distinct & {a,b,c} on P ) by A1, A20, A26, A28, A29, A27, A31, Th21; :: thesis: verum

end;A21: {b,a} on B by A2;

consider D being LINE of G such that

A22: {b,d} on D by A2;

consider C being LINE of G such that

A23: {b,c} on C by A2;

A24: b on D by A22, INCSP_1:1;

A25: b on C by A23, INCSP_1:1;

b on B by A21, INCSP_1:1;

then A26: b on B,C,D by A25, A24;

consider q being POINT of G such that

A27: q on P,C by A3;

b,a,c,d is_a_quadrangle by A5, Th13;

then A28: B,C,D are_mutually_distinct by A21, A23, A22, Th20;

consider p being POINT of G such that

A29: p on P,B by A3;

A30: q on P by A27;

consider r being POINT of G such that

A31: r on P,D by A3;

A32: r on P by A31;

p on P by A29;

then {p,q,r} on P by A30, A32, INCSP_1:2;

hence ex a, b, c being POINT of G st

( a,b,c are_mutually_distinct & {a,b,c} on P ) by A1, A20, A26, A28, A29, A27, A31, Th21; :: thesis: verum

case A33:
c |' P
; :: thesis: ex a, b, c being POINT of G st

( a,b,c are_mutually_distinct & {a,b,c} on P )

( a,b,c are_mutually_distinct & {a,b,c} on P )

consider B being LINE of G such that

A34: {c,a} on B by A2;

consider D being LINE of G such that

A35: {c,d} on D by A2;

consider C being LINE of G such that

A36: {c,b} on C by A2;

A37: c on D by A35, INCSP_1:1;

A38: c on C by A36, INCSP_1:1;

c on B by A34, INCSP_1:1;

then A39: c on B,C,D by A38, A37;

consider q being POINT of G such that

A40: q on P,C by A3;

c,a,b,d is_a_quadrangle by A5, Th13;

then A41: B,C,D are_mutually_distinct by A34, A36, A35, Th20;

consider p being POINT of G such that

A42: p on P,B by A3;

A43: q on P by A40;

consider r being POINT of G such that

A44: r on P,D by A3;

A45: r on P by A44;

p on P by A42;

then {p,q,r} on P by A43, A45, INCSP_1:2;

hence ex a, b, c being POINT of G st

( a,b,c are_mutually_distinct & {a,b,c} on P ) by A1, A33, A39, A41, A42, A40, A44, Th21; :: thesis: verum

end;A34: {c,a} on B by A2;

consider D being LINE of G such that

A35: {c,d} on D by A2;

consider C being LINE of G such that

A36: {c,b} on C by A2;

A37: c on D by A35, INCSP_1:1;

A38: c on C by A36, INCSP_1:1;

c on B by A34, INCSP_1:1;

then A39: c on B,C,D by A38, A37;

consider q being POINT of G such that

A40: q on P,C by A3;

c,a,b,d is_a_quadrangle by A5, Th13;

then A41: B,C,D are_mutually_distinct by A34, A36, A35, Th20;

consider p being POINT of G such that

A42: p on P,B by A3;

A43: q on P by A40;

consider r being POINT of G such that

A44: r on P,D by A3;

A45: r on P by A44;

p on P by A42;

then {p,q,r} on P by A43, A45, INCSP_1:2;

hence ex a, b, c being POINT of G st

( a,b,c are_mutually_distinct & {a,b,c} on P ) by A1, A33, A39, A41, A42, A40, A44, Th21; :: thesis: verum

( a,b,c are_mutually_distinct & {a,b,c} on P ) ; :: thesis: verum