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

(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