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 A1: ( x is finite-period & a is finite-period & x in BranchV a ) ; :: thesis: ord x = ord a
then consider xx being Element of X such that
A3: ( x = xx & a <= xx ) ;
set nx = ord x;
set na = ord a;
( a |^ (ord a) in BCK-part X & ord a <> 0 ) by Def8a, A1;
then A5: ord a >= 1 by NAT_1:14;

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

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

then a |^ 1 in BCK-part X by Def8a, A1;
then a in BCK-part X by Th3;
then consider aa being Element of X such that
B1: ( a = aa & 0. X <= aa ) ;
a in AtomSet X ;
then consider ab being Element of X such that
B3: ( a = ab & ab is atom ) ;
a ` = 0. X by B1, BCIALG_1:def 11;
then a = 0. X by B3, BCIALG_1:def 14;
then x in BCK-part X by A3;
then B7: ( x |^ 1 in BCK-part X & 1 <> 0 ) by Th3;
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 B0, Def8a, A1, B7; :: thesis: verum

end;

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

a |^ (ord a) in BCK-part X by Def8a, A1;
then consider aa being Element of X such that
B1: ( a |^ (ord a) = aa & 0. X <= aa ) ;
0. X in AtomSet X ;
then B2: x ` = a ` by A1, BCIALG_1:37;
(a |^ (ord a)) ` = 0. X by B1, BCIALG_1:def 11;
then (x ` ) |^ (ord a) = 0. X by B2, Th17;
then (x |^ (ord a)) ` = 0. X by Th17b;
then 0. X <= x |^ (ord a) by BCIALG_1:def 11;
then B7: ( x |^ (ord a) in BCK-part X & ord a <> 0 ) by C1;
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 C1: ( x |^ m in BCK-part X & m <> 0 ) ; :: thesis: ord a <= m
then consider xx being Element of X such that
C3: ( x |^ m = xx & 0. X <= xx ) ;
(x |^ m) ` = 0. X by C3, BCIALG_1:def 11;
then (a ` ) |^ m = 0. X by B2, Th17b;
then (a |^ m) ` = 0. X by Th17;
then 0. X <= a |^ m by BCIALG_1:def 11;
then a |^ m in BCK-part X ;
hence ord a <= m by Def8a, A1, C1; :: thesis: verum

end;

hence ord x = ord a by Def8a, A1, B7; :: thesis: verum

end;

end;