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

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