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

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