theorem Th20: :: BCIALG_6:20

for X being BCI-algebra
for x being Element of X
for a being Element of AtomSet X
for n being Nat st a = ((x `) `) |^ n holds
x |^ n in BranchV a