let V be RealLinearSpace; :: thesis: for x, y being VECTOR of V st Gen x,y holds
for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y )
let x, y be VECTOR of V; :: thesis: ( Gen x,y implies for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y ) )
assume A1: Gen x,y ; :: thesis: for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y )
let u, v, w be VECTOR of V; :: thesis: ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y )

A2: now

assume A3: u = v ; :: thesis: ex u1 being M2(the carrier of V) ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y )
take u1 = w + x; :: thesis: ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y )
Ortm x,y,w, Ortm x,y,u1 // u,v by A3, ANALOAF:18;
then A4: w,u1,u,v are_COrtm_wrt x,y by Def4;
w <> u1

proof

assume w = u1 ; :: thesis: contradiction
then x = 0. V by RLVECT_1:22;
hence contradiction by A1, Lm4; :: thesis: verum

end;

hence ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y ) by A1, A4, Th19; :: thesis: verum

end;

now

assume A5: u <> v ; :: thesis: ex u1 being M2(the carrier of V) ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y )
consider u2 being VECTOR of V such that
A6: Ortm x,y,u2 = u by A1, Th8;
consider v2 being VECTOR of V such that
A7: Ortm x,y,v2 = v by A1, Th8;
take u1 = (v2 + w) - u2; :: thesis: ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y )
u2,v2 // w,u1 by ANALOAF:25;
then w,u1 // u2,v2 by ANALOAF:21;
then Ortm x,y,w, Ortm x,y,u1 // Ortm x,y,u2, Ortm x,y,v2 by A1, Th17;
then A8: w,u1,u,v are_COrtm_wrt x,y by A6, A7, Def4;
w <> u1

proof

assume w = u1 ; :: thesis: contradiction
then w = w + (v2 - u2) by RLVECT_1:def 6;
then v2 - u2 = 0. V by RLVECT_1:22;
hence contradiction by A5, A6, A7, RLVECT_1:35; :: thesis: verum

end;

hence ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y ) by A1, A8, Th19; :: thesis: verum

end;

hence ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrtm_wrt x,y ) by A2; :: thesis: verum