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