A1: now :: thesis: for g being Element of G st g in {(1_ G)} holds
g " in {(1_ G)}

let g be Element of G; :: thesis: ( g in {(1_ G)} implies g " in {(1_ G)} )
assume g in {(1_ G)} ; :: thesis: g " in {(1_ G)}
then g = 1_ G by TARSKI:def 1;
then g " = 1_ G by GROUP_1:8;
hence g " in {(1_ G)} by TARSKI:def 1; :: thesis: verum

end;

now :: thesis: for g1, g2 being Element of G st g1 in {(1_ G)} & g2 in {(1_ G)} holds
g1 * g2 in {(1_ G)}

let g1, g2 be Element of G; :: thesis: ( g1 in {(1_ G)} & g2 in {(1_ G)} implies g1 * g2 in {(1_ G)} )
assume ( g1 in {(1_ G)} & g2 in {(1_ G)} ) ; :: thesis: g1 * g2 in {(1_ G)}
then ( g1 = 1_ G & g2 = 1_ G ) by TARSKI:def 1;
then g1 * g2 = 1_ G by GROUP_1:def 4;
hence g1 * g2 in {(1_ G)} by TARSKI:def 1; :: thesis: verum

end;

hence ex b₁ being strict Subgroup of G st the carrier of b₁ = {(1_ G)} by A1, Th52; :: thesis: verum