let G be non empty Group-like multMagma ; :: thesis: for H being Subgroup of G st G is finite holds

H is finite

let H be Subgroup of G; :: thesis: ( G is finite implies H is finite )

assume A1: G is finite ; :: thesis: H is finite

the carrier of H c= the carrier of G by Def5;

hence the carrier of H is finite by A1; :: according to STRUCT_0:def 11 :: thesis: verum

H is finite

let H be Subgroup of G; :: thesis: ( G is finite implies H is finite )

assume A1: G is finite ; :: thesis: H is finite

the carrier of H c= the carrier of G by Def5;

hence the carrier of H is finite by A1; :: according to STRUCT_0:def 11 :: thesis: verum