let G be Group; for B, A being Subgroup of G st B is Subgroup of A holds
commutators A,B c= carr A
let B, A be Subgroup of G; ( B is Subgroup of A implies commutators A,B c= carr A )
assume A1:
B is Subgroup of A
; commutators A,B c= carr A
let x be set ; TARSKI:def 3 ( not x in commutators A,B or x in carr A )
assume
x in commutators A,B
; x in carr A
then consider a, b being Element of G such that
A2:
( x = [.a,b.] & a in A & b in B )
by GROUP_5:58;
A3:
b in A
by A1, A2, GROUP_2:49;
then A4:
a * b in A
by A2, GROUP_2:59;
( a " in A & b " in A )
by A2, A3, GROUP_2:60;
then
(a " ) * (b " ) in A
by GROUP_2:59;
then A5:
((a " ) * (b " )) * (a * b) in A
by A4, GROUP_2:59;
[.a,b.] = ((a " ) * (b " )) * (a * b)
by GROUP_1:def 4;
hence
x in carr A
by A2, A5, STRUCT_0:def 5; verum