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

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