let V be RealLinearSpace; for u, u1, v, v1, x, y being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrte_wrt x,y holds
v,v1,u1,u are_COrte_wrt x,y
let u, u1, v, v1, x, y be VECTOR of V; ( Gen x,y & u,u1,v,v1 are_COrte_wrt x,y implies v,v1,u1,u are_COrte_wrt x,y )
assume A1:
Gen x,y
; ( not u,u1,v,v1 are_COrte_wrt x,y or v,v1,u1,u are_COrte_wrt x,y )
assume
u,u1,v,v1 are_COrte_wrt x,y
; v,v1,u1,u are_COrte_wrt x,y
then
Orte (x,y,u), Orte (x,y,u1) // v,v1
;
then
v,v1 // Orte (x,y,u), Orte (x,y,u1)
by ANALOAF:12;
then
Orte (x,y,v), Orte (x,y,v1) // Orte (x,y,(Orte (x,y,u))), Orte (x,y,(Orte (x,y,u1)))
by A1, Th16;
then
Orte (x,y,v), Orte (x,y,v1) // - u, Orte (x,y,(Orte (x,y,u1)))
by A1, Th14;
then
Orte (x,y,v), Orte (x,y,v1) // - u, - u1
by A1, Th14;
then A2:
- u, - u1 // Orte (x,y,v), Orte (x,y,v1)
by ANALOAF:12;
(- u1) - (- u) =
u + (- u1)
by RLVECT_1:17
.=
u - u1
;
then A3:
- u, - u1 // u1,u
by ANALOAF:15;
A4:
( - u <> - u1 implies v,v1,u1,u are_COrte_wrt x,y )
by A2, A3, ANALOAF:11;
now ( - u = - u1 implies v,v1,u1,u are_COrte_wrt x,y )assume
- u = - u1
;
v,v1,u1,u are_COrte_wrt x,ythen u =
- (- u1)
by RLVECT_1:17
.=
u1
by RLVECT_1:17
;
then
Orte (
x,
y,
v),
Orte (
x,
y,
v1)
// u1,
u
by ANALOAF:9;
hence
v,
v1,
u1,
u are_COrte_wrt x,
y
;
verum end;
hence
v,v1,u1,u are_COrte_wrt x,y
by A4; verum