let H be Subgroup of G; :: thesis: H is associative
let x, y, z be Element of H; :: according to GROUP_1:def 3 :: thesis: (x * y) * z = x * (y * z)
( y * z in the carrier of H & the carrier of H c= the carrier of G ) by Def5;
then reconsider a = x, b = y, c = z, ab = x * y, bc = y * z as Element of G ;
thus (x * y) * z = ab * c by Th43
.= (a * b) * c by Th43
.= a * (b * c) by GROUP_1:def 3
.= a * bc by Th43
.= x * (y * z) by Th43 ; :: thesis: verum