let V be RealLinearSpace; :: thesis: for u, v, x, y being VECTOR of V st Gen x,y holds
Orte (x,y,(u - v)) = (Orte (x,y,u)) - (Orte (x,y,v))
let u, v, x, y be VECTOR of V; :: thesis: ( Gen x,y implies Orte (x,y,(u - v)) = (Orte (x,y,u)) - (Orte (x,y,v)) )
assume A1: Gen x,y ; :: thesis: Orte (x,y,(u - v)) = (Orte (x,y,u)) - (Orte (x,y,v))
hence Orte (x,y,(u - v)) = (Orte (x,y,u)) + (Orte (x,y,(- v))) by Th10
.= (Orte (x,y,u)) - (Orte (x,y,v)) by A1, Th9 ;
:: thesis: verum