:: deftheorem Def3 defines Proportionality_as_EqRel_of ANPROJ_1:def 3 :
for V being RealLinearSpace
for b₂ being Equivalence_Relation of (NonZero V) holds
( b₂ = Proportionality_as_EqRel_of V iff for x, y being object holds
( [x,y] in b₂ iff ( x in NonZero V & y in NonZero V & ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) ) ) );