vect_trig_3D: THEORY
BEGIN

  IMPORTING vectors_3D

  u,v : VAR Nz_vector

  cos(u,v): real = u*v/(norm(u)*norm(v))

  trig_range  : TYPE = {x:real | -1 <= x AND x <= 1}

  cos_range   : JUDGEMENT cos(u,v) HAS_TYPE trig_range

  cos_symm : LEMMA cos(u,v) = cos(v,u)

END vect_trig_3D