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

proof

assume A1: x in AtomSet X ; :: thesis: for z, u being Element of X holds z \ (z \ (x \ u)) = x \ u
let z, u be Element of X; :: thesis: z \ (z \ (x \ u)) = x \ u
x \ u = ((x \ u) `) ` by A1, Th31
.= ((z \ z) \ (x \ u)) ` by Def5
.= ((z \ (x \ u)) \ z) ` by Th7
.= ((z \ (x \ u)) `) \ (z `) by Th9 ;
then A2: (x \ u) \ (z \ (z \ (x \ u))) = 0. X by Th1;
(z \ (z \ (x \ u))) \ (x \ u) = 0. X by Th1;
hence z \ (z \ (x \ u)) = x \ u by A2, Def7; :: thesis: verum

end;

assume for z, u being Element of X holds z \ (z \ (x \ u)) = x \ u ; :: thesis: x in AtomSet X
then for u being Element of X holds ((x \ u) `) ` = x \ u ;
hence x in AtomSet X by Th31; :: thesis: verum