per cases ( G is unital or not G is unital ) ;

suppose G is unital ; :: thesis: not bool G is empty

then bool G = multLoopStr(# (bool the carrier of G),( the multF of G .:^2),{(the_unity_wrt the multF of G)} #) by Def9;
hence not the carrier of (bool G) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum

end;

suppose not G is unital ; :: thesis: not bool G is empty

then bool G = multMagma(# (bool the carrier of G),( the multF of G .:^2) #) by Def9;
hence not the carrier of (bool G) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum

end;

end;