theorem Th20: :: CAYLDICK:20

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