let AS be Oriented_Orthogonality_Space; for u, u1, w being Element of AS holds
( u,u1 // w,w & w,w // u,u1 )
let u, u1, w be Element of AS; ( u,u1 // w,w & w,w // u,u1 )
set v = the Element of AS;
consider v1 being Element of AS such that
A1:
v1 <> the Element of AS
and
A2:
the Element of AS,v1 '//' u,u1
by Def1;
the Element of AS,v1 '//' w,w
by Def1;
hence
( u,u1 // w,w & w,w // u,u1 )
by A1, A2; verum