theorem Th16: :: CAYLDICK:16

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