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

now :: thesis: ( u <> y & y <> v implies u # y,y // y,y # v )

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

end;

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