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