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 )

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

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 & x in H2 )
; :: thesis: x in H1 /\ H2
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;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

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