let X be BCI-algebra; :: thesis: for x being Element of X holds
( x in AtomSet X iff for z being Element of X holds (z \ x) ` = x \ z )
let x be Element of X; :: thesis: ( x in AtomSet X iff for z being Element of X holds (z \ x) ` = x \ z )
A1: ( ( for z being Element of X holds (z `) \ (x `) = x \ z ) implies for z being Element of X holds (z \ x) ` = x \ z )

proof

assume A2: for z being Element of X holds (z `) \ (x `) = x \ z ; :: thesis: for z being Element of X holds (z \ x) ` = x \ z
let z be Element of X; :: thesis: (z \ x) ` = x \ z
(z `) \ (x `) = x \ z by A2;
hence (z \ x) ` = x \ z by Th9; :: thesis: verum

end;

( ( for z being Element of X holds (z \ x) ` = x \ z ) implies for z being Element of X holds (z `) \ (x `) = x \ z )

proof

assume A3: for z being Element of X holds (z \ x) ` = x \ z ; :: thesis: for z being Element of X holds (z `) \ (x `) = x \ z
let z be Element of X; :: thesis: (z `) \ (x `) = x \ z
(z \ x) ` = x \ z by A3;
hence (z `) \ (x `) = x \ z by Th9; :: thesis: verum

end;

hence ( x in AtomSet X iff for z being Element of X holds (z \ x) ` = x \ z ) by A1, Th28; :: thesis: verum