let R be Skew-Field; :: thesis: for s being Element of R holds the carrier of (center R) c= the carrier of (centralizer s)
let s be Element of R; :: thesis: the carrier of (center R) c= the carrier of (centralizer s)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (center R) or x in the carrier of (centralizer s) )
assume A1: x in the carrier of (center R) ; :: thesis: x in the carrier of (centralizer s)
the carrier of (center R) c= the carrier of R by Th16;
then reconsider a = x as Element of R by A1;
a in center R by A1;
then a * s = s * a by Th17;
hence x in the carrier of (centralizer s) by Th24; :: thesis: verum