theorem Th3: :: ANPROJ_1:3

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