let V be RealLinearSpace; :: thesis: for x, y, u, v being VECTOR of V st Gen x,y holds
u,v, Orte x,y,u, Orte x,y,v are_Ort_wrt x,y
let x, y, u, v be VECTOR of V; :: thesis: ( Gen x,y implies u,v, Orte x,y,u, Orte x,y,v are_Ort_wrt x,y )
assume A1: Gen x,y ; :: thesis: u,v, Orte x,y,u, Orte x,y,v are_Ort_wrt x,y
set w = (Orte x,y,v) - (Orte x,y,u);
A2: (Orte x,y,v) - (Orte x,y,u) = Orte x,y,(v - u) by A1, Th11
.= ((pr2 x,y,(v - u)) * x) + ((- (pr1 x,y,(v - u))) * y) ;
PProJ x,y,(v - u),((Orte x,y,v) - (Orte x,y,u)) = ((pr1 x,y,(v - u)) * (pr1 x,y,((Orte x,y,v) - (Orte x,y,u)))) + ((pr2 x,y,(v - u)) * (pr2 x,y,((Orte x,y,v) - (Orte x,y,u)))) by GEOMTRAP:def 6
.= ((pr1 x,y,(v - u)) * (pr2 x,y,(v - u))) + ((pr2 x,y,(v - u)) * (pr2 x,y,((Orte x,y,v) - (Orte x,y,u)))) by A1, A2, Lm6
.= ((pr1 x,y,(v - u)) * (pr2 x,y,(v - u))) + ((- (pr1 x,y,(v - u))) * (pr2 x,y,(v - u))) by A1, A2, Lm6
.= 0 ;
then v - u,(Orte x,y,v) - (Orte x,y,u) are_Ort_wrt x,y by A1, GEOMTRAP:34;
hence u,v, Orte x,y,u, Orte x,y,v are_Ort_wrt x,y by ANALMETR:def 3; :: thesis: verum