let G be Group; :: thesis: for A, B being Subset of G st A c= B holds
Centralizer B is Subgroup of Centralizer A
let A, B be Subset of G; :: thesis: ( A c= B implies Centralizer B is Subgroup of Centralizer A )
assume A1: A c= B ; :: thesis: Centralizer B is Subgroup of Centralizer A
for g being Element of G st g in Centralizer B holds
g in Centralizer A

proof

let g be Element of G; :: thesis: ( g in Centralizer B implies g in Centralizer A )
assume g in Centralizer B ; :: thesis: g in Centralizer A
then for a being Element of G st a in A holds
g * a = a * g by A1, Th57;
then g is Element of (Centralizer A) by Th57;
hence g in Centralizer A ; :: thesis: verum

end;

hence Centralizer B is Subgroup of Centralizer A by GROUP_2:58; :: thesis: verum