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