theorem Th13: :: ANPROJ_1:13

for V being RealLinearSpace
for p, q being Element of V st p + q = 0. V holds
are_Prop p,q