let X be BCI-algebra; :: thesis: for x being Element of X
for a being Element of AtomSet X st x is finite-period & a is finite-period & x in BranchV a holds
ord x = ord a
let x be Element of X; :: thesis: for a being Element of AtomSet X st x is finite-period & a is finite-period & x in BranchV a holds
ord x = ord a
let a be Element of AtomSet X; :: thesis: ( x is finite-period & a is finite-period & x in BranchV a implies ord x = ord a )
assume that
A1: x is finite-period and
A2: a is finite-period and
A3: x in BranchV a ; :: thesis: ord x = ord a
set na = ord a;
ord a <> 0 by A2, Def5;
then A4: ord a >= 1 by NAT_1:14;

per cases ( ord a = 1 or ord a > 1 ) by A4, XXREAL_0:1;

suppose A5: ord a = 1 ; :: thesis: ord x = ord a

then a |^ 1 in BCK-part X by A2, Def5;
then a in BCK-part X by Th4;
then ex aa being Element of X st
( a = aa & 0. X <= aa ) ;
then A6: a ` = 0. X ;
a in AtomSet X ;
then ex ab being Element of X st
( a = ab & ab is atom ) ;
then a = 0. X by A6;
then A7: x |^ 1 in BCK-part X by A3, Th4;
for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds
1 <= m by NAT_1:14;
hence ord x = ord a by A1, A5, A7, Def5; :: thesis: verum

end;

suppose A8: ord a > 1 ; :: thesis: ord x = ord a

0. X in AtomSet X ;
then A9: x ` = a ` by A3, BCIALG_1:37;
A10: for m being Element of NAT st x |^ m in BCK-part X & m <> 0 holds
ord a <= m

proof

let m be Element of NAT ; :: thesis: ( x |^ m in BCK-part X & m <> 0 implies ord a <= m )
assume that
A11: x |^ m in BCK-part X and
A12: m <> 0 ; :: thesis: ord a <= m
ex xx being Element of X st
( x |^ m = xx & 0. X <= xx ) by A11;
then (x |^ m) ` = 0. X ;
then (a `) |^ m = 0. X by A9, Th18;
then (a |^ m) ` = 0. X by Th17;
then 0. X <= a |^ m ;
then a |^ m in BCK-part X ;
hence ord a <= m by A2, A12, Def5; :: thesis: verum

end;

a |^ (ord a) in BCK-part X by A2, Def5;
then ex aa being Element of X st
( a |^ (ord a) = aa & 0. X <= aa ) ;
then (a |^ (ord a)) ` = 0. X ;
then (x `) |^ (ord a) = 0. X by A9, Th17;
then (x |^ (ord a)) ` = 0. X by Th18;
then 0. X <= x |^ (ord a) ;
then x |^ (ord a) in BCK-part X ;
hence ord x = ord a by A1, A8, A10, Def5; :: thesis: verum

end;

end;