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;