let G be addGroup; :: thesis: for H2, H1 being Subgroup of G holds
( H1 is Subgroup of H2 iff addMagma(# the carrier of (H1 /\ H2), the addF of (H1 /\ H2) #) = addMagma(# the carrier of H1, the addF of H1 #) )
let H2, H1 be Subgroup of G; :: thesis: ( H1 is Subgroup of H2 iff addMagma(# the carrier of (H1 /\ H2), the addF of (H1 /\ H2) #) = addMagma(# the carrier of H1, the addF of H1 #) )
thus ( H1 is Subgroup of H2 implies addMagma(# the carrier of (H1 /\ H2), the addF of (H1 /\ H2) #) = addMagma(# the carrier of H1, the addF of H1 #) ) :: thesis: ( addMagma(# the carrier of (H1 /\ H2), the addF of (H1 /\ H2) #) = addMagma(# the carrier of H1, the addF of H1 #) implies H1 is Subgroup of H2 )
proof
assume H1 is Subgroup of H2 ; :: thesis: addMagma(# the carrier of (H1 /\ H2), the addF of (H1 /\ H2) #) = addMagma(# the carrier of H1, the addF of H1 #)
then A1: the carrier of H1 c= the carrier of H2 by DefA5;
the carrier of (H1 /\ H2) = (carr H1) /\ (carr H2) by Def10;
hence addMagma(# the carrier of (H1 /\ H2), the addF of (H1 /\ H2) #) = addMagma(# the carrier of H1, the addF of H1 #) by A1, Th59, XBOOLE_1:28; :: thesis: verum
end;
assume addMagma(# the carrier of (H1 /\ H2), the addF of (H1 /\ H2) #) = addMagma(# the carrier of H1, the addF of H1 #) ; :: thesis: 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