theorem :: CAYLDICK:18

for N being non empty ConjNormAlgStr
for a, b being Element of N st a is complementable & b is complementable holds
<%a,b%> is complementable by Th14, Th16;