for V being RealLinearSpace
for w, y being VECTOR of V
for p, p1, p2, q being Element of (AMSpace (V,w,y)) st Gen w,y & p,q _|_ p1,p2 & p1,q _|_ p2,p holds
p2,q _|_ p,p1