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 that
A3: u <> v and
A4: u1 <> v1 ; :: thesis: 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; :: 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