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