let G be Group; :: thesis: for H being Subgroup of G holds
( H is trivial iff for x being Element of G holds
( x in H iff x = 1_ G ) )
let H be Subgroup of G; :: thesis: ( H is trivial iff for x being Element of G holds
( x in H iff x = 1_ G ) )
thus ( H is trivial implies for x being Element of G holds
( x in H iff x = 1_ G ) ) :: thesis: ( ( for x being Element of G holds
( x in H iff x = 1_ G ) ) implies H is trivial )

proof

assume H is trivial ; :: thesis: for x being Element of G holds
( x in H iff x = 1_ G )
then consider h being object such that
A1: the carrier of H = {h} by GROUP_6:def 2;
1_ H in {h} by A1;
then 1_ H = h by TARSKI:def 1;
then A2: the carrier of H = {(1_ H)} by A1;
let x be Element of G; :: thesis: ( x in H iff x = 1_ G )

hereby :: thesis: ( x = 1_ G implies x in H )

assume x in H ; :: thesis: x = 1_ G
then x in {(1_ H)} by A2;
then x = 1_ H by TARSKI:def 1;
hence x = 1_ G by GROUP_2:44; :: thesis: verum

end;

assume x = 1_ G ; :: thesis: x in H
then x = 1_ H by GROUP_2:44;
hence x in H ; :: thesis: verum

end;

assume A3: for x being Element of G holds
( x in H iff x = 1_ G ) ; :: thesis: H is trivial
for x being object holds
( x in the carrier of H iff x = 1_ G )

proof

let x be object ; :: thesis: ( x in the carrier of H iff x = 1_ G )

hereby :: thesis: ( x = 1_ G implies x in the carrier of H )

assume x in the carrier of H ; :: thesis: x = 1_ G
then A4: x in H ;
then x in G by GROUP_2:40;
hence x = 1_ G by A3, A4; :: thesis: verum

end;

assume x = 1_ G ; :: thesis: x in the carrier of H
then x in H by A3;
hence x in the carrier of H ; :: thesis: verum

end;

then the carrier of H = {(1_ G)} by TARSKI:def 1;
hence H is trivial ; :: thesis: verum