let x be object ; :: thesis: for G being Group
for H1, H2 being Subgroup of G holds
( x in H1 /\ H2 iff ( x in H1 & x in H2 ) )
let G be Group; :: 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 the carrier of (H1 /\ H2) ;
then x in (carr H1) /\ (carr H2) by Def10;
then ( x in carr H1 & x in carr H2 ) by XBOOLE_0:def 4;
hence ( x in H1 & x in H2 ) ; :: thesis: verum

end;

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