for N being non empty ConjNormAlgStr
for a, b being Element of N st <%a,b%> is complementable holds
( a is complementable & b is complementable ) by Th15, Th17;