let V be RealLinearSpace; :: thesis: 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 )
let x, y be object ; :: thesis: ( [x,y] in Proportionality_as_EqRel_of V implies ( x is Element of V & y is Element of V ) )
assume [x,y] in Proportionality_as_EqRel_of V ; :: thesis: ( x is Element of V & y is Element of V )
then ex u, v being Element of V st
( x = u & y = v & are_Prop u,v ) by Def3;
then reconsider x = x, y = y as Element of V ;
( x is Element of V & y is Element of V ) ;
hence ( x is Element of V & y is Element of V ) ; :: thesis: verum