let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
for p, q, r being Element of (AMSpace V,w,y) holds p,q _|_ r,r
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies for p, q, r being Element of (AMSpace V,w,y) holds p,q _|_ r,r )
assume A1: Gen w,y ; :: thesis: for p, q, r being Element of (AMSpace V,w,y) holds p,q _|_ r,r
let p, q, r be Element of (AMSpace V,w,y); :: thesis: p,q _|_ r,r
reconsider u = p, v = q, u1 = r as Element of V ;
u1 - u1 = 0. V by RLVECT_1:28;
then v - u,u1 - u1 are_Ort_wrt w,y by A1, Th9;
then u,v,u1,u1 are_Ort_wrt w,y by Def3;
hence p,q _|_ r,r by Th31; :: thesis: verum