let X be BCI-algebra; :: thesis: for x, y being Element of X
for a being Element of AtomSet X st x \ y is finite-period & x in BranchV a & y in BranchV a holds
ord (x \ y) = 1
let x, y be Element of X; :: thesis: for a being Element of AtomSet X st x \ y is finite-period & x in BranchV a & y in BranchV a holds
ord (x \ y) = 1
let a be Element of AtomSet X; :: thesis: ( x \ y is finite-period & x in BranchV a & y in BranchV a implies ord (x \ y) = 1 )
assume A1: ( x \ y is finite-period & x in BranchV a & y in BranchV a ) ; :: thesis: ord (x \ y) = 1
then x \ y in BCK-part X by BCIALG_1:40;
then A3: (x \ y) |^ 1 in BCK-part X by Th3;
for m being Element of NAT st (x \ y) |^ m in BCK-part X & m <> 0 holds
1 <= m by NAT_1:14;
hence ord (x \ y) = 1 by Def8a, A3, A1; :: thesis: verum