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 that
A1: x \ y is finite-period and
A2: ( x in BranchV a & y in BranchV a ) ; :: thesis: ord (x \ y) = 1
A3: for m being Element of NAT st (x \ y) |^ m in BCK-part X & m <> 0 holds
1 <= m by NAT_1:14;
x \ y in BCK-part X by A2, BCIALG_1:40;
then (x \ y) |^ 1 in BCK-part X by Th4;
hence ord (x \ y) = 1 by A1, A3, Def5; :: thesis: verum