let O be set ; :: thesis: for G being strict GroupWithOperators of O st G is trivial holds
(1). G = G
let G be strict GroupWithOperators of O; :: thesis: ( G is trivial implies (1). G = G )
reconsider H = G as StableSubgroup of G by Lm3;
assume G is trivial ; :: thesis: (1). G = G
then ex x being object st the carrier of G = {x} ;
then the carrier of H = {(1_ G)} by TARSKI:def 1;
hence (1). G = G by Def8; :: thesis: verum