let AS be Oriented_Orthogonality_Space; :: thesis: for u, u1, v, v1 being Element of AS st u,u1 // v,v1 holds
v,v1 // u,u1
let u, u1, v, v1 be Element of AS; :: thesis: ( u,u1 // v,v1 implies v,v1 // u,u1 )
assume u,u1 // v,v1 ; :: thesis: v,v1 // u,u1
then ex w, w1 being Element of AS st
( w <> w1 & w,w1 '//' u,u1 & w,w1 '//' v,v1 ) by Def3;
hence v,v1 // u,u1 by Def3; :: thesis: verum