let V be RealLinearSpace; :: thesis: for x, y, u, v, u1, v1, w being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,u1,w are_COrte_wrt x,y & not u,v,v1,w are_COrte_wrt x,y holds
u,v,w,v1 are_COrte_wrt x,y
let x, y, u, v, u1, v1, w be VECTOR of V; :: thesis: ( Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,u1,w are_COrte_wrt x,y & not u,v,v1,w are_COrte_wrt x,y implies u,v,w,v1 are_COrte_wrt x,y )
assume A1:
( Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,u1,w are_COrte_wrt x,y )
; :: thesis: ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y )
then A2:
( Orte x,y,u, Orte x,y,v // u1,v1 & Orte x,y,u, Orte x,y,v // u1,w )
by Def3;
now assume A3:
u <> v
;
:: thesis: ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y )now assume A4:
(
u1 <> v1 &
u1 <> w )
;
:: thesis: ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y )A5:
u1,
v1 // u1,
w
by A1, A2, A3, Th13, ANALOAF:20;
A6:
now assume A7:
u1,
v1 // v1,
w
;
:: thesis: ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y )
u1,
v1 // Orte x,
y,
u,
Orte x,
y,
v
by A2, ANALOAF:21;
then
Orte x,
y,
u,
Orte x,
y,
v // v1,
w
by A4, A7, ANALOAF:20;
hence
(
u,
v,
v1,
w are_COrte_wrt x,
y or
u,
v,
w,
v1 are_COrte_wrt x,
y )
by Def3;
:: thesis: verum end; now assume A8:
u1,
w // w,
v1
;
:: thesis: ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y )
u1,
w // Orte x,
y,
u,
Orte x,
y,
v
by A2, ANALOAF:21;
then
Orte x,
y,
u,
Orte x,
y,
v // w,
v1
by A4, A8, ANALOAF:20;
hence
(
u,
v,
v1,
w are_COrte_wrt x,
y or
u,
v,
w,
v1 are_COrte_wrt x,
y )
by Def3;
:: thesis: verum end; hence
(
u,
v,
v1,
w are_COrte_wrt x,
y or
u,
v,
w,
v1 are_COrte_wrt x,
y )
by A5, A6, ANALOAF:23;
:: thesis: verum end; hence
(
u,
v,
v1,
w are_COrte_wrt x,
y or
u,
v,
w,
v1 are_COrte_wrt x,
y )
by A1;
:: thesis: verum end;
hence
( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y )
by Th20; :: thesis: verum