let x be object ; :: thesis: for G being addGroup
for H1, H2 being Subgroup of G holds
( x in H1 /\ H2 iff ( x in H1 & x in H2 ) )
let G be addGroup; :: thesis: for H1, H2 being Subgroup of G holds
( x in H1 /\ H2 iff ( x in H1 & x in H2 ) )
let H1, H2 be Subgroup of G; :: thesis: ( x in H1 /\ H2 iff ( x in H1 & x in H2 ) )
thus ( x in H1 /\ H2 implies ( x in H1 & x in H2 ) ) :: thesis: ( x in H1 & x in H2 implies x in H1 /\ H2 )

proof

assume x in H1 /\ H2 ; :: thesis: ( x in H1 & x in H2 )
then x in (carr H1) /\ (carr H2) by Def10;
hence ( x in H1 & x in H2 ) by XBOOLE_0:def 4; :: thesis: verum

end;

assume ( x in H1 & x in H2 ) ; :: thesis: x in H1 /\ H2
then x in (carr H1) /\ (carr H2) ;
hence x in H1 /\ H2 by Def10; :: thesis: verum