theorem Th2: :: ANPROJ_1:2

for V being RealLinearSpace
for p, q, u being Element of V st are_Prop p,u & are_Prop u,q holds
are_Prop p,q