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

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

end;

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

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

end;

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