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 & w,w1,v,v1 are_COrtm_wrt x,y & w,w1,u2,v2 are_COrtm_wrt x,y & not w = w1 & not v = v1 holds
u,u1,u2,v2 are_COrtm_wrt x,y
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 & w,w1,v,v1 are_COrtm_wrt x,y & w,w1,u2,v2 are_COrtm_wrt x,y & not w = w1 & not v = v1 implies u,u1,u2,v2 are_COrtm_wrt x,y )
assume A1:
Gen x,y
; ( not u,u1,v,v1 are_COrtm_wrt x,y or not w,w1,v,v1 are_COrtm_wrt x,y or not w,w1,u2,v2 are_COrtm_wrt x,y or w = w1 or v = v1 or u,u1,u2,v2 are_COrtm_wrt x,y )
assume that
A2:
u,u1,v,v1 are_COrtm_wrt x,y
and
A3:
w,w1,v,v1 are_COrtm_wrt x,y
and
A4:
w,w1,u2,v2 are_COrtm_wrt x,y
; ( w = w1 or v = v1 or u,u1,u2,v2 are_COrtm_wrt x,y )
Ortm (x,y,u), Ortm (x,y,u1) // v,v1
by A2;
then A5:
v,v1 // Ortm (x,y,u), Ortm (x,y,u1)
by ANALOAF:12;
Ortm (x,y,w), Ortm (x,y,w1) // v,v1
by A3;
then A6:
v,v1 // Ortm (x,y,w), Ortm (x,y,w1)
by ANALOAF:12;
A7:
Ortm (x,y,w), Ortm (x,y,w1) // u2,v2
by A4;
now ( w <> w1 & v <> v1 implies u,u1,u2,v2 are_COrtm_wrt x,y )assume that A8:
w <> w1
and A9:
v <> v1
;
u,u1,u2,v2 are_COrtm_wrt x,y
Ortm (
x,
y,
w),
Ortm (
x,
y,
w1)
// Ortm (
x,
y,
u),
Ortm (
x,
y,
u1)
by A5, A6, A9, ANALOAF:11;
then
Ortm (
x,
y,
u),
Ortm (
x,
y,
u1)
// u2,
v2
by A1, A7, A8, Th6, ANALOAF:11;
hence
u,
u1,
u2,
v2 are_COrtm_wrt x,
y
;
verum end;
hence
( w = w1 or v = v1 or u,u1,u2,v2 are_COrtm_wrt x,y )
; verum