theorem :: CAYLDICK:25

for N being non empty ConjNormAlgStr
for a, b being Element of N st <%a,b%> is add-cancelable holds
( a is add-cancelable & b is add-cancelable ) by Th21, Th23;