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