theorem Th15: :: CAYLDICK:15

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