theorem Th23: :: CAYLDICK:23
for N being non empty ConjNormAlgStr
for a, b being Element of N st <%a,b%> is right_add-cancelable holds
( a is right_add-cancelable & b is right_add-cancelable )