let V be RealLinearSpace; :: thesis: for u, v, y being VECTOR of V st u,y // y,v holds
( v,y // y,u & u,y // u,v & y,v // u,v )
let u, v, y 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:12;
hence A2: v,y // y,u by ANALOAF:12; :: thesis: ( u,y // u,v & y,v // u,v )
thus u,y // u,v by A1, ANALOAF:13; :: thesis: y,v // u,v
v,y // v,u by A2, ANALOAF:13;
hence y,v // u,v by ANALOAF:12; :: thesis: verum