for V being RealLinearSpace
for w, y being VECTOR of V
for p, p1 being Element of (AMSpace (V,w,y)) st Gen w,y & p <> p1 holds
for q being Element of (AMSpace (V,w,y)) ex q1 being Element of (AMSpace (V,w,y)) st
( p,p1 // p,q1 & p,p1 _|_ q1,q )