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
Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1)
let u, u1, v, v1, x, y be VECTOR of V; :: thesis: ( Gen x,y & u,v // u1,v1 implies Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1) )
assume A1: Gen x,y ; :: thesis: ( not u,v // u1,v1 or Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1) )
assume A2: u,v // u1,v1 ; :: thesis: Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1)

now :: thesis: ( u <> v implies Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1) )

assume A3: u <> v ; :: thesis: Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1)

now :: thesis: ( u1 <> v1 implies Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1) )

assume u1 <> v1 ; :: thesis: Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1)
then consider a, b being Real such that
A4: 0 < a and
A5: 0 < b and
A6: a * (v - u) = b * (v1 - u1) by A2, A3, ANALOAF:def 1;
a * ((Ortm (x,y,v)) - (Ortm (x,y,u))) = a * (Ortm (x,y,(v - u))) by A1, Th5
.= Ortm (x,y,(b * (v1 - u1))) by A1, A6, Th2
.= b * (Ortm (x,y,(v1 - u1))) by A1, Th2
.= b * ((Ortm (x,y,v1)) - (Ortm (x,y,u1))) by A1, Th5 ;
hence Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1) by A4, A5, ANALOAF:def 1; :: thesis: verum

end;

hence Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1) by ANALOAF:9; :: thesis: verum

end;

hence Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1) by ANALOAF:9; :: thesis: verum