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 & u,u1,u2,v2 are_COrte_wrt x,y & not u2,v2,w,w1 are_COrte_wrt x,y & not v = v1 holds
u = u1
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 & u,u1,u2,v2 are_COrte_wrt x,y & not u2,v2,w,w1 are_COrte_wrt x,y & not v = v1 implies u = u1 )
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 u,u1,u2,v2 are_COrte_wrt x,y or u2,v2,w,w1 are_COrte_wrt x,y or v = v1 or u = u1 )
assume A2:
( u,u1,v,v1 are_COrte_wrt x,y & v,v1,w,w1 are_COrte_wrt x,y & u,u1,u2,v2 are_COrte_wrt x,y )
; :: thesis: ( u2,v2,w,w1 are_COrte_wrt x,y or v = v1 or u = u1 )
then A3:
Orte x,y,u, Orte x,y,u1 // v,v1
by Def3;
A4:
Orte x,y,v, Orte x,y,v1 // w,w1
by A2, Def3;
A5:
Orte x,y,u, Orte x,y,u1 // u2,v2
by A2, Def3;
now assume A6:
(
u <> u1 &
v <> v1 )
;
:: thesis: ( u2,v2,w,w1 are_COrte_wrt x,y or v = v1 or u = u1 )then
v,
v1 // u2,
v2
by A1, A3, A5, Th13, ANALOAF:20;
then
Orte x,
y,
v,
Orte x,
y,
v1 // Orte x,
y,
u2,
Orte x,
y,
v2
by A1, Th16;
then
Orte x,
y,
u2,
Orte x,
y,
v2 // w,
w1
by A1, A4, A6, Th13, ANALOAF:20;
hence
(
u2,
v2,
w,
w1 are_COrte_wrt x,
y or
v = v1 or
u = u1 )
by Def3;
:: thesis: verum end;
hence
( u2,v2,w,w1 are_COrte_wrt x,y or v = v1 or u = u1 )
; :: thesis: verum