let V be RealLinearSpace; 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; ( Gen x,y implies ex v being VECTOR of V st Orte (x,y,v) = u )
assume A1:
Gen x,y
; ex v being VECTOR of V st Orte (x,y,v) = u
take v = - (Orte (x,y,u)); 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
; verum