let V be RealLinearSpace; :: thesis: for u, y, v being VECTOR of V st u,y // y,v holds
u # y,y // y,y # v
let u, y, v be VECTOR of V; :: thesis: ( u,y // y,v implies u # y,y // y,y # v )
assume A1: u,y // y,v ; :: thesis: u # y,y // y,y # v
set p = u # y;
set q = y # v;
( u,u # y // u # y,y & y,y # v // y # v,v ) by Th13;
then ( u # y,y // u,y & y,y # v // y,v ) by Lm1;
then A2: ( u,y // u # y,y & y,v // y,y # v ) by ANALOAF:21;

now

assume that
A3: u <> y and
A4: y <> v ; :: thesis: u # y,y // y,y # v
y,v // u # y,y by A1, A2, A3, ANALOAF:20;
hence u # y,y // y,y # v by A2, A4, ANALOAF:20; :: thesis: verum

end;

hence u # y,y // y,y # v by ANALOAF:18; :: thesis: verum