theorem Th9:
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 lie_on_an_angle &
o,
u,
v,
w,
u2,
v2,
w2 are_half_mutually_not_Prop &
u,
v2,
w1 are_LinDep &
u2,
v,
w1 are_LinDep &
u,
w2,
v1 are_LinDep &
w,
u2,
v1 are_LinDep &
v,
w2,
u1 are_LinDep &
w,
v2,
u1 are_LinDep holds
u1,
v1,
w1 are_LinDep