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

proof

assume x in AtomSet X ; :: thesis: for u, z being Element of X holds (z \ u) \ (z \ x) = x \ u
then A1: ex x1 being Element of X st
( x = x1 & x1 is atom ) ;
let u, z be Element of X; :: thesis: (z \ u) \ (z \ x) = x \ u
(z \ (z \ x)) \ x = 0. X by Th1;
then z \ (z \ x) = x by A1;
hence (z \ u) \ (z \ x) = x \ u by Th7; :: thesis: verum

end;

assume A2: for u, z being Element of X holds (z \ u) \ (z \ x) = x \ u ; :: thesis: x in AtomSet X

now :: thesis: for z being Element of X st z \ x = 0. X holds
z = x

let z be Element of X; :: thesis: ( z \ x = 0. X implies z = x )
assume z \ x = 0. X ; :: thesis: z = x
then (z \ (0. X)) \ (0. X) = x \ (0. X) by A2;
then (z \ (0. X)) \ (0. X) = x by Th2;
then z \ (0. X) = x by Th2;
hence z = x by Th2; :: thesis: verum

end;

then x is atom ;
hence x in AtomSet X ; :: thesis: verum