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

proof

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

end;

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

now

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

end;

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