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

( 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