let X be BCI-algebra; :: thesis: for a being Element of AtomSet X holds (a |^ (- 1)) |^ (- 1) = a
let a be Element of AtomSet X; :: thesis: (a |^ (- 1)) |^ (- 1) = a
(a |^ (- 1)) |^ (- 1) = (a `) |^ (- 1) by Th5
.= (a `) ` by Th5 ;
hence (a |^ (- 1)) |^ (- 1) = a by BCIALG_1:29; :: thesis: verum