let V be RealLinearSpace; :: thesis: 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; :: 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 :: thesis: ( 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 ; :: 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:9; :: thesis: verum