let AS be Oriented_Orthogonality_Space; :: thesis: 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; :: thesis: ( u,u1 // w,w & w,w // u,u1 )
consider v being Element of AS;
consider v1 being Element of AS such that
A1: v1 <> v and
A2: v,v1 '//' u,u1 by Def1;
v,v1 '//' w,w by Def1;
hence ( u,u1 // w,w & w,w // u,u1 ) by A1, A2, Def3; :: thesis: verum