theorem Th22: :: CAYLDICK:22

for N being non empty ConjNormAlgStr
for a, b being Element of N st a is right_add-cancelable & b is right_add-cancelable holds
<%a,b%> is right_add-cancelable