let X be BCI-algebra; 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; ( 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) )
( ( 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
;
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;
(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;
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)
;
verum
end;
assume A2:
for y, z, u being Element of X holds (x \ u) \ (z \ y) <= (y \ u) \ (z \ x)
; x in AtomSet X
then
x is atom
;
hence
x in AtomSet X
; verum