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

end;

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;hence not the carrier of (bool G) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum