let V be RealLinearSpace; 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; ( 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
; u # y,y // y,y # v
now ( u <> y & y <> v implies u # y,y // y,y # v )assume that A4:
u <> y
and A5:
y <> v
;
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;
verum end;
hence
u # y,y // y,y # v
by ANALOAF:9; verum