theorem Th1: :: ANPROJ_1:1

for V being RealLinearSpace
for p, q being Element of V holds
( are_Prop p,q iff ex a being Real st
( a <> 0 & p = a * q ) )