let G be Group; :: thesis: for H2, H1 being Subgroup of G holds

( H1 is Subgroup of H2 iff multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) )

let H2, H1 be Subgroup of G; :: thesis: ( H1 is Subgroup of H2 iff multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) )

thus ( H1 is Subgroup of H2 implies multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) ) :: thesis: ( multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) implies H1 is Subgroup of H2 )

then the carrier of H1 = (carr H1) /\ (carr H2) by Def10

.= the carrier of H1 /\ the carrier of H2 ;

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

( H1 is Subgroup of H2 iff multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) )

let H2, H1 be Subgroup of G; :: thesis: ( H1 is Subgroup of H2 iff multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) )

thus ( H1 is Subgroup of H2 implies multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) ) :: thesis: ( multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) implies H1 is Subgroup of H2 )

proof

assume
multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #)
; :: thesis: H1 is Subgroup of H2
assume
H1 is Subgroup of H2
; :: thesis: multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #)

then A1: the carrier of H1 c= the carrier of H2 by Def5;

the carrier of (H1 /\ H2) = (carr H1) /\ (carr H2) by Def10;

hence multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) by A1, Th59, XBOOLE_1:28; :: thesis: verum

end;then A1: the carrier of H1 c= the carrier of H2 by Def5;

the carrier of (H1 /\ H2) = (carr H1) /\ (carr H2) by Def10;

hence multMagma(# the carrier of (H1 /\ H2), the multF of (H1 /\ H2) #) = multMagma(# the carrier of H1, the multF of H1 #) by A1, Th59, XBOOLE_1:28; :: thesis: verum

then the carrier of H1 = (carr H1) /\ (carr H2) by Def10

.= the carrier of H1 /\ the carrier of H2 ;

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