let G be Group; :: thesis: for H1, H2 being Subgroup of G st the carrier of H1 c= the carrier of H2 holds

H1 is Subgroup of H2

let H1, H2 be Subgroup of G; :: thesis: ( the carrier of H1 c= the carrier of H2 implies H1 is Subgroup of H2 )

set A = the carrier of H1;

set B = the carrier of H2;

set h = the multF of G;

assume A1: the carrier of H1 c= the carrier of H2 ; :: thesis: H1 is Subgroup of H2

hence the carrier of H1 c= the carrier of H2 ; :: according to GROUP_2:def 5 :: thesis: the multF of H1 = the multF of H2 || the carrier of H1

A2: [: the carrier of H1, the carrier of H1:] c= [: the carrier of H2, the carrier of H2:] by A1, ZFMISC_1:96;

( the multF of H1 = the multF of G || the carrier of H1 & the multF of H2 = the multF of G || the carrier of H2 ) by Def5;

hence the multF of H1 = the multF of H2 || the carrier of H1 by A2, FUNCT_1:51; :: thesis: verum

H1 is Subgroup of H2

let H1, H2 be Subgroup of G; :: thesis: ( the carrier of H1 c= the carrier of H2 implies H1 is Subgroup of H2 )

set A = the carrier of H1;

set B = the carrier of H2;

set h = the multF of G;

assume A1: the carrier of H1 c= the carrier of H2 ; :: thesis: H1 is Subgroup of H2

hence the carrier of H1 c= the carrier of H2 ; :: according to GROUP_2:def 5 :: thesis: the multF of H1 = the multF of H2 || the carrier of H1

A2: [: the carrier of H1, the carrier of H1:] c= [: the carrier of H2, the carrier of H2:] by A1, ZFMISC_1:96;

( the multF of H1 = the multF of G || the carrier of H1 & the multF of H2 = the multF of G || the carrier of H2 ) by Def5;

hence the multF of H1 = the multF of H2 || the carrier of H1 by A2, FUNCT_1:51; :: thesis: verum