let G be addGroup; :: thesis: for H1, H2 being Subgroup of G holds
( ( for H being Subgroup of G st H = H1 /\ H2 holds
the carrier of H = the carrier of H1 /\ the carrier of H2 ) & ( for H being strict Subgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds
H = H1 /\ H2 ) )
let H1, H2 be Subgroup of G; :: thesis: ( ( for H being Subgroup of G st H = H1 /\ H2 holds
the carrier of H = the carrier of H1 /\ the carrier of H2 ) & ( for H being strict Subgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds
H = H1 /\ H2 ) )
A1: ( the carrier of H1 = carr H1 & the carrier of H2 = carr H2 ) ;
thus for H being Subgroup of G st H = H1 /\ H2 holds
the carrier of H = the carrier of H1 /\ the carrier of H2 :: thesis: for H being strict Subgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds
H = H1 /\ H2
proof
let H be Subgroup of G; :: thesis: ( H = H1 /\ H2 implies the carrier of H = the carrier of H1 /\ the carrier of H2 )
assume H = H1 /\ H2 ; :: thesis: the carrier of H = the carrier of H1 /\ the carrier of H2
hence the carrier of H = (carr H1) /\ (carr H2) by Def10
.= the carrier of H1 /\ the carrier of H2 ;
:: thesis: verum
end;
let H be strict Subgroup of G; :: thesis: ( the carrier of H = the carrier of H1 /\ the carrier of H2 implies H = H1 /\ H2 )
assume the carrier of H = the carrier of H1 /\ the carrier of H2 ; :: thesis: H = H1 /\ H2
hence H = H1 /\ H2 by A1, Def10; :: thesis: verum