( H2(R) is Abelian & H2(R) is add-associative & H2(R) is right_zeroed & H2(R) is right_complementable ) by Lm5;
hence ex b1 being non empty RightModStr over R st
( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict ) ; :: thesis: verum