let G be addGroup; :: thesis: for H1, H2 being Subgroup of G st ( for g being Element of G st g in H1 holds
g in H2 ) holds
H1 is Subgroup of H2
let H1, H2 be Subgroup of G; :: thesis: ( ( for g being Element of G st g in H1 holds
g in H2 ) implies H1 is Subgroup of H2 )
assume A1: for g being Element of G st g in H1 holds
g in H2 ; :: thesis: H1 is Subgroup of H2
the carrier of H1 c= the carrier of H2

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of H1 or x in the carrier of H2 )
assume x in the carrier of H1 ; :: thesis: x in the carrier of H2
then reconsider g = x as Element of H1 ;
reconsider g = g as Element of G by Th41, STRUCT_0:def 5;
g in H1 ;
then g in H2 by A1;
hence x in the carrier of H2 ; :: thesis: verum

end;

hence H1 is Subgroup of H2 by Th57; :: thesis: verum