theorem Th20: :: ANPROJ_1:20

for V being RealLinearSpace
for u, v being Element of V holds
( [u,v] in Proportionality_as_EqRel_of V iff ( not u is zero & not v is zero & are_Prop u,v ) )