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