let V be RealLinearSpace; :: thesis: for p, q being Element of V st p + q = 0. V holds
are_Prop p,q
let p, q be Element of V; :: thesis: ( p + q = 0. V implies are_Prop p,q )
assume p + q = 0. V ; :: thesis: are_Prop p,q
then q = - p by RLVECT_1:def 10;
then q = (- 1) * p by RLVECT_1:16;
hence are_Prop p,q by Th1; :: thesis: verum