let G be Group; for A, B being Subgroup of G st B is Subgroup of A holds
commutators (A,B) c= carr A
let A, B 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 object ; 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:52;
A3:
b in A
by A1, A2, GROUP_2:40;
then A4:
a * b in A
by A2, GROUP_2:50;
( a " in A & b " in A )
by A2, A3, GROUP_2:51;
then
(a ") * (b ") in A
by GROUP_2:50;
then A5:
((a ") * (b ")) * (a * b) in A
by A4, GROUP_2:50;
[.a,b.] = ((a ") * (b ")) * (a * b)
by GROUP_1:def 3;
hence
x in carr A
by A2, A5, STRUCT_0:def 5; verum