let V be RealLinearSpace; :: thesis: for u, y, v being VECTOR of V st u,y // y,v holds
( v,y // y,u & u,y // u,v & y,v // u,v )
let u, y, v be VECTOR of V; :: thesis: ( u,y // y,v implies ( v,y // y,u & u,y // u,v & y,v // u,v ) )
assume A1: u,y // y,v ; :: thesis: ( v,y // y,u & u,y // u,v & y,v // u,v )
then y,u // v,y by ANALOAF:21;
hence A2: v,y // y,u by ANALOAF:21; :: thesis: ( u,y // u,v & y,v // u,v )
thus u,y // u,v by A1, ANALOAF:22; :: thesis: y,v // u,v
v,y // v,u by A2, ANALOAF:22;
hence y,v // u,v by ANALOAF:21; :: thesis: verum