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 )
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; :: thesis: verum