let X be BCI-algebra; :: thesis: for x, y being Element of X
for a, b being Element of AtomSet X st x \ y is finite-period & a \ b is finite-period & x is finite-period & y is finite-period & a is finite-period & b is finite-period & a <> b & x in BranchV a & y in BranchV b holds
ord (a \ b) divides (ord x) lcm (ord y)
let x, y be Element of X; :: thesis: for a, b being Element of AtomSet X st x \ y is finite-period & a \ b is finite-period & x is finite-period & y is finite-period & a is finite-period & b is finite-period & a <> b & x in BranchV a & y in BranchV b holds
ord (a \ b) divides (ord x) lcm (ord y)
let a, b be Element of AtomSet X; :: thesis: ( x \ y is finite-period & a \ b is finite-period & x is finite-period & y is finite-period & a is finite-period & b is finite-period & a <> b & x in BranchV a & y in BranchV b implies ord (a \ b) divides (ord x) lcm (ord y) )
assume A1: ( x \ y is finite-period & a \ b is finite-period & x is finite-period & y is finite-period & a is finite-period & b is finite-period & a <> b & x in BranchV a & y in BranchV b ) ; :: thesis: ord (a \ b) divides (ord x) lcm (ord y)
A6: ( ord x divides (ord x) lcm (ord y) & ord y divides (ord x) lcm (ord y) ) by NAT_D:def 4;
then consider xy being Nat such that
A7: (ord x) lcm (ord y) = (ord x) * xy by NAT_D:def 3;
consider yx being Nat such that
A8: (ord x) lcm (ord y) = (ord y) * yx by A6, NAT_D:def 3;
reconsider xly = (ord x) lcm (ord y) as Element of NAT ;
reconsider na = ord a, nb = ord b as Element of NAT ;
reconsider nab = ord (a \ b) as Element of NAT ;
(a \ b) |^ xly = (a |^ ((ord x) * xy)) \ (b |^ ((ord y) * yx)) by A8, A7, Th16
.= ((a |^ (ord x)) |^ xy) \ (b |^ ((ord y) * yx)) by Th21
.= ((a |^ (ord x)) |^ xy) \ ((b |^ (ord y)) |^ yx) by Th21
.= ((a |^ na) |^ xy) \ ((b |^ (ord y)) |^ yx) by A1, Th25
.= ((0. X) |^ xy) \ ((b |^ (ord y)) |^ yx) by Th23, A1
.= ((0. X) |^ xy) \ ((b |^ (ord b)) |^ yx) by A1, Th25
.= ((0. X) |^ xy) \ ((0. X) |^ yx) by Th23, A1
.= ((0. X) |^ yx) ` by Th6
.= (0. X) ` by Th6
.= 0. X by BCIALG_1:def 5 ;
then ((a \ b) |^ xly) ` = 0. X by BCIALG_1:def 5;
then 0. X <= (a \ b) |^ xly by BCIALG_1:def 11;
then (a \ b) |^ xly in BCK-part X ;
hence ord (a \ b) divides (ord x) lcm (ord y) by Th26, A1; :: thesis: verum