let R be Skew-Field; :: thesis: for s being Element of R holds the carrier of (centralizer s) c= the carrier of R
let s be Element of R; :: thesis: the carrier of (centralizer s) c= the carrier of R
set cs = centralizer s;
set ccs = the carrier of (centralizer s);
A1: the carrier of (centralizer s) = { x where x is Element of R : x * s = s * x } by Def5;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (centralizer s) or x in the carrier of R )
assume x in the carrier of (centralizer s) ; :: thesis: x in the carrier of R
then ex a being Element of R st
( a = x & a * s = s * a ) by A1;
hence x in the carrier of R ; :: thesis: verum