consider mo being Relation of {0};
consider mF being Function of [: the carrier of F,{0}:],{0};
( SymStr(# {0},md,o,mF,mo #) is Abelian & SymStr(# {0},md,o,mF,mo #) is add-associative & SymStr(# {0},md,o,mF,mo #) is right_zeroed & SymStr(# {0},md,o,mF,mo #) is right_complementable ) by Lm3;
hence ex b₁ being non empty SymStr of F st
( b₁ is Abelian & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable ) ; :: thesis: verum