:: deftheorem defines are_parallel DUALSP06:def 4 :
for V being RealNormSpace
for x being Point of V
for y being Point of (DualSp V) holds
( x,y are_parallel iff x .|. y = ||.x.|| * ||.y.|| );