theorem Th9: :: ANPROJ11:9

for u, v being non zero Element of (TOP-REAL 3)
for r being Real st r <> 0 & are_Prop u,v holds
are_Prop r * u,v