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 )

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
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
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 ) ) )
per cases ( a |' P or b |' P or c |' P ) by ;
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 )

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 ;
A12: a on C by ;
a on B by ;
then A13: a on B,C,D by ;
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 ;
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;
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 )

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 ;
A25: b on C by ;
b on B by ;
then A26: b on B,C,D by ;
consider q being POINT of G such that
A27: q on P,C by A3;
then A28: B,C,D are_mutually_distinct by ;
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 ;
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;
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 )

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 ;
A38: c on C by ;
c on B by ;
then A39: c on B,C,D by ;
consider q being POINT of G such that
A40: q on P,C by A3;
then A41: B,C,D are_mutually_distinct by ;
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 ;
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;
end;
end;
hence ex a, b, c being POINT of G st
( a,b,c are_mutually_distinct & {a,b,c} on P ) ; :: thesis: verum
end;
end;