let V be RealLinearSpace; :: thesis: for x, y, u, u1, v, v1, w, w1, u2, v2 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 x, y, u, u1, v, v1, w, w1, u2, v2 be VECTOR of V; :: thesis: ( 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
; :: thesis: ( 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 A2:
( 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 )
; :: thesis: ( u,u1,u2,v2 are_COrte_wrt x,y or v = v1 or w = w1 )
then
v,v1,u1,u are_COrte_wrt x,y
by A1, Th18;
then A3:
Orte x,y,v, Orte x,y,v1 // u1,u
by Def3;
Orte x,y,v, Orte x,y,v1 // w,w1
by A2, Def3;
then A4:
w,w1 // Orte x,y,v, Orte x,y,v1
by ANALOAF:21;
Orte x,y,u2, Orte x,y,v2 // w,w1
by A2, Def3;
then A5:
w,w1 // Orte x,y,u2, Orte x,y,v2
by ANALOAF:21;
now assume A6:
(
w <> w1 &
v <> v1 )
;
:: thesis: ( u,u1,u2,v2 are_COrte_wrt x,y or v = v1 or w = w1 )then
Orte x,
y,
v,
Orte x,
y,
v1 // Orte x,
y,
u2,
Orte x,
y,
v2
by A4, A5, ANALOAF:20;
then
Orte x,
y,
u2,
Orte x,
y,
v2 // u1,
u
by A1, A3, A6, Th13, ANALOAF:20;
then
Orte x,
y,
v2,
Orte x,
y,
u2 // u,
u1
by ANALOAF:21;
then
v2,
u2,
u,
u1 are_COrte_wrt x,
y
by Def3;
hence
(
u,
u1,
u2,
v2 are_COrte_wrt x,
y or
v = v1 or
w = w1 )
by A1, Th18;
:: thesis: verum end;
hence
( u,u1,u2,v2 are_COrte_wrt x,y or v = v1 or w = w1 )
; :: thesis: verum