theorem Th17: :: CAYLDICK:17

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