let X be BCI-algebra; :: thesis: for x being Element of X st x is nilpotent holds
ord x = ord (x ` )
let x be Element of X; :: thesis: ( x is nilpotent implies ord x = ord (x ` ) )
assume A1: x is nilpotent ; :: thesis: ord x = ord (x ` )
then consider k being non empty Element of NAT such that
A2: (0. X),x to_power k = 0. X by Def6;
A3: x ` is nilpotent

proof

take k ; :: according to BCIALG_2:def 6 :: thesis: (0. X),(x ` ) to_power k = 0. X
(0. X),(x ` ) to_power k = ((0. X),x to_power k) ` by Th9
.= 0. X by A2, BCIALG_1:def 5 ;
hence (0. X),(x ` ) to_power k = 0. X ; :: thesis: verum

end;

set k = ord x;
ord (x ` ) = ord x

proof

A4: (0. X),(x ` ) to_power (ord x) = ((0. X),x to_power (ord x)) ` by Th9
.= (0. X) ` by A1, Def8
.= 0. X by BCIALG_1:def 5 ;

now

let m be Element of NAT ; :: thesis: ( (0. X),(x ` ) to_power m = 0. X & m <> 0 implies ord x <= m )
assume A5: ( (0. X),(x ` ) to_power m = 0. X & m <> 0 ) ; :: thesis: ord x <= m
then ((0. X),x to_power m) ` = 0. X by Th9;
then (((0. X),x to_power m) ` ) ` = 0. X by BCIALG_1:def 5;
then (0. X),x to_power m = 0. X by Th12;
hence ord x <= m by A1, A5, Def8; :: thesis: verum

end;

hence ord (x ` ) = ord x by A3, A4, Def8; :: thesis: verum

end;

hence ord x = ord (x ` ) ; :: thesis: verum