theorem :: ANPROJ_1:19

for V being RealLinearSpace
for x, y being object st [x,y] in Proportionality_as_EqRel_of V holds
( x is Element of V & y is Element of V )