:: deftheorem defines lie_on_an_angle ANPROJ_2:def 4 :
for V being RealLinearSpace
for o, u, v, w, u2, v2, w2 being Element of V holds
( o,u,v,w,u2,v2,w2 lie_on_an_angle iff ( not o,u,u2 are_LinDep & o,u,v are_LinDep & o,u,w are_LinDep & o,u2,v2 are_LinDep & o,u2,w2 are_LinDep ) );