let V be non trivial RealLinearSpace; for x, d, b, b9, d9, q being Element of (ProjectiveSpace V) st not q,b,d are_collinear & b,d,x are_collinear & q,b9,b are_collinear & q,d9,d are_collinear holds
ex o being Element of (ProjectiveSpace V) st
( b9,d9,o are_collinear & q,x,o are_collinear )
let x, d, b, b9, d9, q be Element of (ProjectiveSpace V); ( not q,b,d are_collinear & b,d,x are_collinear & q,b9,b are_collinear & q,d9,d are_collinear implies ex o being Element of (ProjectiveSpace V) st
( b9,d9,o are_collinear & q,x,o are_collinear ) )
assume that
A1:
not q,b,d are_collinear
and
A2:
b,d,x are_collinear
and
A3:
q,b9,b are_collinear
and
A4:
q,d9,d are_collinear
; ex o being Element of (ProjectiveSpace V) st
( b9,d9,o are_collinear & q,x,o are_collinear )
A5:
b9,q,b are_collinear
by A3, Th24;
A6:
b <> d
by A1, Def7;
A7:
now ( b <> b9 implies ex o being Element of (ProjectiveSpace V) st
( b9,d9,o are_collinear & q,x,o are_collinear ) )A8:
b,
b9,
q are_collinear
by A3, Th24;
consider z being
Element of
(ProjectiveSpace V) such that A9:
b9,
d9,
z are_collinear
and A10:
b,
d,
z are_collinear
by A4, A5, Def9;
A11:
z,
b9,
b9 are_collinear
by Def7;
b,
d,
b are_collinear
by Def7;
then
z,
b,
x are_collinear
by A2, A6, A10, Def8;
then consider o being
Element of
(ProjectiveSpace V) such that A12:
z,
b9,
o are_collinear
and A13:
x,
q,
o are_collinear
by A8, Def9;
A14:
q,
x,
o are_collinear
by A13, Th24;
assume A15:
b <> b9
;
ex o being Element of (ProjectiveSpace V) st
( b9,d9,o are_collinear & q,x,o are_collinear )A16:
z <> b9
proof
assume
not
z <> b9
;
contradiction
then A17:
b,
b9,
d are_collinear
by A10, Th24;
(
b,
b9,
q are_collinear &
b,
b9,
b are_collinear )
by A3, Def7, Th24;
hence
contradiction
by A1, A15, A17, Def8;
verum
end;
z,
b9,
d9 are_collinear
by A9, Th24;
then
b9,
d9,
o are_collinear
by A12, A16, A11, Def8;
hence
ex
o being
Element of
(ProjectiveSpace V) st
(
b9,
d9,
o are_collinear &
q,
x,
o are_collinear )
by A14;
verum end;
now ( b = b9 implies ex o being Element of (ProjectiveSpace V) st
( b9,d9,o are_collinear & q,x,o are_collinear ) )assume
b = b9
;
ex o being Element of (ProjectiveSpace V) st
( b9,d9,o are_collinear & q,x,o are_collinear )then A18:
d,
b9,
x are_collinear
by A2, Th24;
d9,
d,
q are_collinear
by A4, Th24;
then consider o being
Element of
(ProjectiveSpace V) such that A19:
d9,
b9,
o are_collinear
and A20:
q,
x,
o are_collinear
by A18, Def9;
b9,
d9,
o are_collinear
by A19, Th24;
hence
ex
o being
Element of
(ProjectiveSpace V) st
(
b9,
d9,
o are_collinear &
q,
x,
o are_collinear )
by A20;
verum end;
hence
ex o being Element of (ProjectiveSpace V) st
( b9,d9,o are_collinear & q,x,o are_collinear )
by A7; verum