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 Th4
.= (a ` ) ` by Th4 ;
hence (a |^ (- 1)) |^ (- 1) = a by BCIALG_1:29; :: thesis: verum