let R be finite Skew-Field; :: thesis: for s being Element of R holds 1 < card the carrier of (centralizer s)
let s be Element of R; :: thesis: 1 < card the carrier of (centralizer s)
A1: card {(0. R),(1. R)} = 2 by CARD_2:57;
A2: 0. R is Element of (centralizer s) by Th27;
1_ R is Element of (centralizer s) by Th27;
then {(0. R),(1_ R)} c= the carrier of (centralizer s) by A2, ZFMISC_1:32;
then 2 <= card the carrier of (centralizer s) by A1, NAT_1:43;
hence 1 < card the carrier of (centralizer s) by XXREAL_0:2; :: thesis: verum