let G be Group; :: thesis: for H, K being strict characteristic Subgroup of G holds H /\ K is characteristic Subgroup of G
let H, K be strict characteristic Subgroup of G; :: thesis: H /\ K is characteristic Subgroup of G
for phi being Automorphism of G
for x being Element of G st x in H /\ K holds
phi . x in H /\ K

proof

let phi be Automorphism of G; :: thesis: for x being Element of G st x in H /\ K holds
phi . x in H /\ K
let x be Element of G; :: thesis: ( x in H /\ K implies phi . x in H /\ K )
assume x in H /\ K ; :: thesis: phi . x in H /\ K
then B1: ( x in H & x in K ) by GROUP_2:82;
then B2: phi . x in H by Th50;
phi . x in K by B1, Th50;
hence phi . x in H /\ K by B2, GROUP_2:82; :: thesis: verum

end;

hence H /\ K is characteristic Subgroup of G by Th50; :: thesis: verum