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 )
( ( for z being Element of X holds (z \ x) ` = x \ z ) iff for z being Element of X holds (z ` ) \ (x ` ) = x \ z )

proof

thus ( ( for z being Element of X holds (z \ x) ` = x \ z ) implies for z being Element of X holds (z ` ) \ (x ` ) = x \ z ) :: thesis: ( ( 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 A1: 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 A1;
hence (z ` ) \ (x ` ) = x \ z by Th9; :: thesis: verum

end;

thus ( ( for z being Element of X holds (z ` ) \ (x ` ) = x \ z ) implies for z being Element of X holds (z \ x) ` = x \ z ) :: thesis: verum

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;

end;

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