let V be RealLinearSpace; :: thesis: for x, y, u, u1, v, v1, w, w1, u2, v2 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 & u2,v2,w,w1 are_COrtm_wrt x,y & not u,u1,u2,v2 are_COrtm_wrt x,y & not v = v1 holds
w = w1
let x, y, u, u1, v, v1, w, w1, u2, v2 be VECTOR of V; :: thesis: ( Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y & v,v1,w,w1 are_COrtm_wrt x,y & u2,v2,w,w1 are_COrtm_wrt x,y & not u,u1,u2,v2 are_COrtm_wrt x,y & not v = v1 implies w = w1 )
assume A1:
Gen x,y
; :: thesis: ( not u,u1,v,v1 are_COrtm_wrt x,y or not v,v1,w,w1 are_COrtm_wrt x,y or not u2,v2,w,w1 are_COrtm_wrt x,y or u,u1,u2,v2 are_COrtm_wrt x,y or v = v1 or w = w1 )
assume A2:
( u,u1,v,v1 are_COrtm_wrt x,y & v,v1,w,w1 are_COrtm_wrt x,y & u2,v2,w,w1 are_COrtm_wrt x,y )
; :: thesis: ( u,u1,u2,v2 are_COrtm_wrt x,y or v = v1 or w = w1 )
then
Ortm x,y,u, Ortm x,y,u1 // v,v1
by Def4;
then A3:
v,v1 // Ortm x,y,u, Ortm x,y,u1
by ANALOAF:21;
w,w1,v,v1 are_COrtm_wrt x,y
by A1, A2, Th19;
then
Ortm x,y,w, Ortm x,y,w1 // v,v1
by Def4;
then A4:
v,v1 // Ortm x,y,w, Ortm x,y,w1
by ANALOAF:21;
w,w1,u2,v2 are_COrtm_wrt x,y
by A1, A2, Th19;
then A5:
Ortm x,y,w, Ortm x,y,w1 // u2,v2
by Def4;
now assume A6:
(
w <> w1 &
v <> v1 )
;
:: thesis: ( u,u1,u2,v2 are_COrtm_wrt x,y or v = v1 or w = w1 )then
Ortm x,
y,
w,
Ortm x,
y,
w1 // Ortm x,
y,
u,
Ortm x,
y,
u1
by A3, A4, ANALOAF:20;
then
Ortm x,
y,
u,
Ortm x,
y,
u1 // u2,
v2
by A1, A5, A6, Th6, ANALOAF:20;
hence
(
u,
u1,
u2,
v2 are_COrtm_wrt x,
y or
v = v1 or
w = w1 )
by Def4;
:: thesis: verum end;
hence
( u,u1,u2,v2 are_COrtm_wrt x,y or v = v1 or w = w1 )
; :: thesis: verum