theorem Th30:
for
V being non
trivial RealLinearSpace st ex
y,
u,
v,
w being
Element of
V st
( ( for
w1 being
Element of
V ex
a,
b,
a1,
b1 being
Real st
w1 = (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) ) & ( for
a,
b,
a1,
b1 being
Real st
(((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds
(
a = 0 &
b = 0 &
a1 = 0 &
b1 = 0 ) ) ) holds
ex
p,
q1,
q2 being
Element of
(ProjectiveSpace V) st
( not
p,
q1,
q2 are_collinear & ( for
r1,
r2 being
Element of
(ProjectiveSpace V) ex
q3,
r3 being
Element of
(ProjectiveSpace V) st
(
r1,
r2,
r3 are_collinear &
q1,
q2,
q3 are_collinear &
p,
r3,
q3 are_collinear ) ) )