let V be RealLinearSpace; :: thesis: for x, y, u, v, u1, v1, w being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,w are_COrtm_wrt x,y holds
u,v,u1,w are_COrtm_wrt x,y
let x, y, u, v, u1, v1, w be VECTOR of V; :: thesis: ( Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,w are_COrtm_wrt x,y implies u,v,u1,w are_COrtm_wrt x,y )
assume A1:
Gen x,y
; :: thesis: ( not u,v,u1,v1 are_COrtm_wrt x,y or not u,v,v1,w are_COrtm_wrt x,y or u,v,u1,w are_COrtm_wrt x,y )
assume A2:
( u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,w are_COrtm_wrt x,y )
; :: thesis: u,v,u1,w are_COrtm_wrt x,y
then A3:
( Ortm x,y,u, Ortm x,y,v // u1,v1 & Ortm x,y,u, Ortm x,y,v // v1,w )
by Def4;
then A4:
u1,v1 // Ortm x,y,u, Ortm x,y,v
by ANALOAF:21;
A5:
now assume
u <> v
;
:: thesis: u,v,u1,w are_COrtm_wrt x,ythen
u1,
v1 // v1,
w
by A1, A3, Th6, ANALOAF:20;
then A6:
u1,
v1 // u1,
w
by ANALOAF:22;
now assume
u1 <> v1
;
:: thesis: u,v,u1,w are_COrtm_wrt x,ythen
Ortm x,
y,
u,
Ortm x,
y,
v // u1,
w
by A4, A6, ANALOAF:20;
hence
u,
v,
u1,
w are_COrtm_wrt x,
y
by Def4;
:: thesis: verum end; hence
u,
v,
u1,
w are_COrtm_wrt x,
y
by A2;
:: thesis: verum end;
now assume
u = v
;
:: thesis: u,v,u1,w are_COrtm_wrt x,ythen
Ortm x,
y,
u,
Ortm x,
y,
v // u1,
w
by ANALOAF:18;
hence
u,
v,
u1,
w are_COrtm_wrt x,
y
by Def4;
:: thesis: verum end;
hence
u,v,u1,w are_COrtm_wrt x,y
by A5; :: thesis: verum