theorem Th21: :: CAYLDICK:21

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