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 DOMAIN_1:sch 7();
A1:
now for a, b being Element of G st a in A & b in A holds
a * b in Alet a,
b be
Element of
G;
( a in A & b in A implies a * b in A )assume that A2:
a in A
and A3:
b in A
;
a * b in Aconsider 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;
hence
a * b in A
;
verum end;
A8:
now for a being Element of G st a in A holds
a " in Alet a be
Element of
G;
( a in A implies a " in A )assume
a in A
;
a " in Athen consider b being
Element of
G such that A9:
b = a
and A10:
for
c being
Element of
G holds
b * c = c * b
;
hence
a " in A
;
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 A1, A8, GROUP_2:52; verum