let V be RealLinearSpace; for u, u1, v, v1, x, y 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 u, u1, v, v1, x, y be VECTOR of V; ( 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
; ( 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
; Orte (x,y,u), Orte (x,y,v) // Orte (x,y,u1), Orte (x,y,v1)
now ( u <> v & u1 <> v1 implies Orte (x,y,u), Orte (x,y,v) // Orte (x,y,u1), Orte (x,y,v1) )assume that A3:
u <> v
and A4:
u1 <> v1
;
Orte (x,y,u), Orte (x,y,v) // Orte (x,y,u1), Orte (x,y,v1)consider a,
b being
Real such that A5:
0 < a
and A6:
0 < b
and A7:
a * (v - u) = b * (v1 - u1)
by A2, A3, A4, 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, A7, 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 A5, A6, ANALOAF:def 1;
verum end;
hence
Orte (x,y,u), Orte (x,y,v) // Orte (x,y,u1), Orte (x,y,v1)
by ANALOAF:9; verum