let H be Subgroup of G; :: thesis: H is associative
let x, y, z be Element of H; :: according to GROUP_1:def 4 :: thesis: (x * y) * z = x * (y * z)
A1: ( x in the carrier of H & y in the carrier of H ) ;
A2: ( z in the carrier of H & x * y in the carrier of H ) ;
( 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 by A1, A2;
thus (x * y) * z = ab * c by Th52
.= (a * b) * c by Th52
.= a * (b * c) by GROUP_1:def 4
.= a * bc by Th52
.= x * (y * z) by Th52 ; :: thesis: verum