let V be RealLinearSpace; :: thesis: for x, y, u, v, u1, v1 being VECTOR of V st Gen x,y & u,v // u1,v1 holds
Orte x,y,u, Orte x,y,v // Orte x,y,u1, Orte x,y,v1
let x, y, u, v, u1, v1 be VECTOR of V; :: thesis: ( Gen x,y & u,v // u1,v1 implies Orte x,y,u, Orte x,y,v // Orte x,y,u1, Orte x,y,v1 )
assume A1:
Gen x,y
; :: thesis: ( not u,v // u1,v1 or Orte x,y,u, Orte x,y,v // Orte x,y,u1, Orte x,y,v1 )
assume A2:
u,v // u1,v1
; :: thesis: Orte x,y,u, Orte x,y,v // Orte x,y,u1, Orte x,y,v1
now assume
(
u <> v &
u1 <> v1 )
;
:: thesis: Orte x,y,u, Orte x,y,v // Orte x,y,u1, Orte x,y,v1then consider a,
b being
Real such that A3:
(
0 < a &
0 < b )
and A4:
a * (v - u) = b * (v1 - u1)
by A2, ANALOAF:def 1;
a * ((Orte x,y,v) - (Orte x,y,u)) =
a * (Orte x,y,(v - u))
by A1, Th11
.=
Orte x,
y,
(b * (v1 - u1))
by A1, A4, Th12
.=
b * (Orte x,y,(v1 - u1))
by A1, Th12
.=
b * ((Orte x,y,v1) - (Orte x,y,u1))
by A1, Th11
;
hence
Orte x,
y,
u,
Orte x,
y,
v // Orte x,
y,
u1,
Orte x,
y,
v1
by A3, ANALOAF:def 1;
:: thesis: verum end;
hence
Orte x,y,u, Orte x,y,v // Orte x,y,u1, Orte x,y,v1
by ANALOAF:18; :: thesis: verum