( H₃(R1,R2) is Abelian & H₃(R1,R2) is add-associative & H₃(R1,R2) is right_zeroed & H₃(R1,R2) is right_complementable ) by Lm6;
hence ex b₁ being non empty BiModStr over R1,R2 st
( b₁ is Abelian & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable & b₁ is strict ) ; :: thesis: verum