for V being RealLinearSpace
for p being Element of V holds
( are_Prop p, 0. V iff p = 0. V ) by RLVECT_1:11;