theorem Th8:
for
V being
RealLinearSpace for
o,
u,
v,
w,
u1,
v1,
w1,
u2,
v2,
w2 being
Element of
V st not
o is
zero &
u,
v,
w are_Prop_Vect &
u2,
v2,
w2 are_Prop_Vect &
u1,
v1,
w1 are_Prop_Vect &
o,
u,
v,
w,
u2,
v2,
w2 are_perspective & not
are_Prop o,
u2 & not
are_Prop o,
v2 & not
are_Prop o,
w2 & not
are_Prop u,
u2 & not
are_Prop v,
v2 & not
are_Prop w,
w2 & not
o,
u,
v are_LinDep & not
o,
u,
w are_LinDep & not
o,
v,
w are_LinDep &
u,
v,
w,
u1,
v1,
w1 lie_on_a_triangle &
u2,
v2,
w2,
u1,
v1,
w1 lie_on_a_triangle holds
u1,
v1,
w1 are_LinDep