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