theorem :: DIRORT:7

for AS being Oriented_Orthogonality_Space
for u, u1, w being Element of AS holds
( u,u1 // w,w & w,w // u,u1 )