:: deftheorem defines are_Prop ANPROJ_1:def 1 :
for V being RealLinearSpace
for p, q being Element of V holds
( are_Prop p,q iff ex a, b being Real st
( a * p = b * q & a <> 0 & b <> 0 ) );