let V be RealLinearSpace; for u, u1, v, v1, x, y being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,u1 are_COrtm_wrt x,y & not u = v holds
u1 = v1
let u, u1, v, v1, x, y be VECTOR of V; ( Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,u1 are_COrtm_wrt x,y & not u = v implies u1 = v1 )
assume A1:
Gen x,y
; ( not u,v,u1,v1 are_COrtm_wrt x,y or not u,v,v1,u1 are_COrtm_wrt x,y or u = v or u1 = v1 )
assume that
A2:
u,v,u1,v1 are_COrtm_wrt x,y
and
A3:
u,v,v1,u1 are_COrtm_wrt x,y
; ( u = v or u1 = v1 )
assume that
A4:
u <> v
and
A5:
u1 <> v1
; contradiction
A6:
Ortm (x,y,u), Ortm (x,y,v) // u1,v1
by A2;
A7:
Ortm (x,y,u), Ortm (x,y,v) // v1,u1
by A3;
Ortm (x,y,u) <> Ortm (x,y,v)
by A1, A4, Th6;
hence
contradiction
by A5, A6, A7, ANALOAF:10, ANALOAF:11; verum