:: deftheorem Def2 defines trivial GROUP_6:def 2 :
for G being non empty 1-sorted holds
( G is trivial iff ex x being object st the carrier of G = {x} );