let V be RealLinearSpace; :: thesis: for x, y being set st [x,y] in Proportionality_as_EqRel_of V holds
( x is Element of & y is Element of )
let x, y be set ; :: thesis: ( [x,y] in Proportionality_as_EqRel_of V implies ( x is Element of & y is Element of ) )
assume [x,y] in Proportionality_as_EqRel_of V ; :: thesis: ( x is Element of & y is Element of )
then ex u, v being Element of st
( x = u & y = v & are_Prop u,v ) by Def5;
then reconsider x = x, y = y as Element of ;
( x is Element of & y is Element of ) ;
hence ( x is Element of & y is Element of ) ; :: thesis: verum