let V be RealLinearSpace; :: thesis: for u, x, y being VECTOR of V st Gen x,y holds
ex v being VECTOR of V st Orte (x,y,v) = u
let u, x, y be VECTOR of V; :: thesis: ( Gen x,y implies ex v being VECTOR of V st Orte (x,y,v) = u )
assume A1: Gen x,y ; :: thesis: ex v being VECTOR of V st Orte (x,y,v) = u
take v = - (Orte (x,y,u)); :: thesis: Orte (x,y,v) = u
thus Orte (x,y,v) = - (Orte (x,y,(Orte (x,y,u)))) by A1, Th9
.= - (- u) by A1, Th14
.= u by RLVECT_1:17 ; :: thesis: verum