theorem :: CAYLDICK:24

for N being non empty ConjNormAlgStr
for a, b being Element of N st a is add-cancelable & b is add-cancelable holds
<%a,b%> is add-cancelable by Th20, Th22;