let G be Group; :: thesis: for A being Subgroup of G holds gr (carr A) is Subgroup of A
let A be Subgroup of G; :: thesis: gr (carr A) is Subgroup of A
set A9 = multMagma(# the carrier of A, the multF of A #);
( the carrier of multMagma(# the carrier of A, the multF of A #) c= the carrier of G & the multF of multMagma(# the carrier of A, the multF of A #) = the multF of G || the carrier of A ) by GROUP_2:def 5;
then reconsider A9 = multMagma(# the carrier of A, the multF of A #) as strict Subgroup of G by GROUP_2:def 5;
A1: gr (carr A) is Subgroup of A9 by GROUP_4:def 4;
A9 is Subgroup of A by GROUP_2:57;
hence gr (carr A) is Subgroup of A by A1, GROUP_2:56; :: thesis: verum