let G be IncProjStr ; ( 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
; 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 verum
let P be
LINE of
G;
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 )
verumproof
now ( ( 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 A6, Th5;
case A7:
a |' P
;
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 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;
verum end; case A20:
b |' P
;
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 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;
verum end; case A33:
c |' P
;
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 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;
verum end;
hence
ex
a,
b,
c being
POINT of
G st
(
a,
b,
c are_mutually_distinct &
{a,b,c} on P )
;
verum
end;
end;