defpred S₁[ Element of G] means for b being Element of G holds $1 * b = b * $1;
reconsider A = { a where a is Element of G : S₁[a] } as Subset of G from DOMAIN_1:sch 7();

A1: now :: thesis: for a, b being Element of G st a in A & b in A holds
a * b in A

let a, b be Element of G; :: thesis: ( a in A & b in A implies a * b in A )
assume that
A2: a in A and
A3: b in A ; :: thesis: a * b in A
consider c being Element of G such that
A4: c = a and
A5: for b being Element of G holds c * b = b * c by A2;
consider d being Element of G such that
A6: d = b and
A7: for a being Element of G holds d * a = a * d by A3;

now :: thesis: for e being Element of G holds (a * b) * e = e * (a * b)

let e be Element of G; :: thesis: (a * b) * e = e * (a * b)
thus (a * b) * e = a * (b * e) by GROUP_1:def 3
.= a * (e * d) by A6, A7
.= (a * e) * b by A6, GROUP_1:def 3
.= (e * c) * b by A4, A5
.= e * (a * b) by A4, GROUP_1:def 3 ; :: thesis: verum

end;

hence a * b in A ; :: thesis: verum

end;

A8: now :: thesis: for a being Element of G st a in A holds
a " in A

let a be Element of G; :: thesis: ( a in A implies a " in A )
assume a in A ; :: thesis: a " in A
then consider b being Element of G such that
A9: b = a and
A10: for c being Element of G holds b * c = c * b ;

now :: thesis: for c being Element of G holds (a ") * c = c * (a ")

let c be Element of G; :: thesis: (a ") * c = c * (a ")
thus (a ") * c = (((a ") * c) ") "
.= ((c ") * ((a ") ")) " by GROUP_1:17
.= ((c ") * b) " by A9
.= (b * (c ")) " by A10
.= (((a ") ") * (c ")) " by A9
.= ((c * (a ")) ") " by GROUP_1:17
.= c * (a ") ; :: thesis: verum

end;

hence a " in A ; :: thesis: verum

end;

now :: thesis: for b being Element of G holds (1_ G) * b = b * (1_ G)

let b be Element of G; :: thesis: (1_ G) * b = b * (1_ G)
(1_ G) * b = b by GROUP_1:def 4;
hence (1_ G) * b = b * (1_ G) by GROUP_1:def 4; :: thesis: verum

end;

then 1_ G in A ;
hence ex b₁ being strict Subgroup of G st the carrier of b₁ = { a where a is Element of G : for b being Element of G holds a * b = b * a } by A1, A8, GROUP_2:52; :: thesis: verum