let AS be Oriented_Orthogonality_Space; :: thesis: for u, u1, v, v1 being Element of AS st u,u1 // v,v1 holds
u1,u // v1,v
let u, u1, v, v1 be Element of AS; :: thesis: ( u,u1 // v,v1 implies u1,u // v1,v )
assume u,u1 // v,v1 ; :: thesis: u1,u // v1,v
then consider w, w1 being Element of AS such that
A1: w <> w1 and
A2: w,w1 '//' u,u1 and
A3: w,w1 '//' v,v1 ;
A4: w1,w '//' v1,v by A3, Def1;
w1,w '//' u1,u by A2, Def1;
hence u1,u // v1,v by A1, A4; :: thesis: verum