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_different & {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_different & {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_different & {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, Def6;
thus
ex
a,
b,
c being
POINT of
G st
(
a,
b,
c are_mutually_different &
{a,b,c} on P )
:: thesis: verumproof
now per cases
( a |' P or b |' P or c |' P )
by A6, Th5;
case A7:
a |' P
;
:: thesis: ex a, b, c being POINT of G st
( a,b,c are_mutually_different & {a,b,c} on P )consider B being
LINE of
G such that A8:
{a,b} on B
by A2;
consider C being
LINE of
G such that A9:
{a,c} on C
by A2;
consider D being
LINE of
G such that A10:
{a,d} on D
by A2;
(
a on B &
a on C &
a on D )
by A8, A9, A10, INCSP_1:11;
then A11:
a on B,
C,
D
by Def3;
A12:
B,
C,
D are_mutually_different
by A5, A8, A9, A10, Th20;
consider p being
POINT of
G such that A13:
p on P,
B
by A3;
consider q being
POINT of
G such that A14:
q on P,
C
by A3;
consider r being
POINT of
G such that A15:
r on P,
D
by A3;
(
p on P &
q on P &
r on P )
by A13, A14, A15, Def2;
then
{p,q,r} on P
by INCSP_1:12;
hence
ex
a,
b,
c being
POINT of
G st
(
a,
b,
c are_mutually_different &
{a,b,c} on P )
by A1, A7, A11, A12, A13, A14, A15, Th21;
:: thesis: verum end; case A16:
b |' P
;
:: thesis: ex a, b, c being POINT of G st
( a,b,c are_mutually_different & {a,b,c} on P )consider B being
LINE of
G such that A17:
{b,a} on B
by A2;
consider C being
LINE of
G such that A18:
{b,c} on C
by A2;
consider D being
LINE of
G such that A19:
{b,d} on D
by A2;
(
b on B &
b on C &
b on D )
by A17, A18, A19, INCSP_1:11;
then A20:
b on B,
C,
D
by Def3;
b,
a,
c,
d is_a_quadrangle
by A5, Th13;
then A21:
B,
C,
D are_mutually_different
by A17, A18, A19, Th20;
consider p being
POINT of
G such that A22:
p on P,
B
by A3;
consider q being
POINT of
G such that A23:
q on P,
C
by A3;
consider r being
POINT of
G such that A24:
r on P,
D
by A3;
(
p on P &
q on P &
r on P )
by A22, A23, A24, Def2;
then
{p,q,r} on P
by INCSP_1:12;
hence
ex
a,
b,
c being
POINT of
G st
(
a,
b,
c are_mutually_different &
{a,b,c} on P )
by A1, A16, A20, A21, A22, A23, A24, Th21;
:: thesis: verum end; case A25:
c |' P
;
:: thesis: ex a, b, c being POINT of G st
( a,b,c are_mutually_different & {a,b,c} on P )consider B being
LINE of
G such that A26:
{c,a} on B
by A2;
consider C being
LINE of
G such that A27:
{c,b} on C
by A2;
consider D being
LINE of
G such that A28:
{c,d} on D
by A2;
(
c on B &
c on C &
c on D )
by A26, A27, A28, INCSP_1:11;
then A29:
c on B,
C,
D
by Def3;
c,
a,
b,
d is_a_quadrangle
by A5, Th13;
then A30:
B,
C,
D are_mutually_different
by A26, A27, A28, Th20;
consider p being
POINT of
G such that A31:
p on P,
B
by A3;
consider q being
POINT of
G such that A32:
q on P,
C
by A3;
consider r being
POINT of
G such that A33:
r on P,
D
by A3;
(
p on P &
q on P &
r on P )
by A31, A32, A33, Def2;
then
{p,q,r} on P
by INCSP_1:12;
hence
ex
a,
b,
c being
POINT of
G st
(
a,
b,
c are_mutually_different &
{a,b,c} on P )
by A1, A25, A29, A30, A31, A32, A33, Th21;
:: thesis: verum end;
hence
ex
a,
b,
c being
POINT of
G st
(
a,
b,
c are_mutually_different &
{a,b,c} on P )
;
:: thesis: verum
end;
end;