defpred S1[ Element of G] means for b being Element of G holds \$1 * b = b * \$1;
reconsider A = { a where a is Element of G : S1[a] } as Subset of G from
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
.= (e * c) * b by A4, A5
.= e * (a * b) by ; :: 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 b1 being strict Subgroup of G st the carrier of b1 = { a where a is Element of G : for b being Element of G holds a * b = b * a } by ; :: thesis: verum