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 ((x \ z) `) ` = x \ z )

let x be Element of X; :: thesis: ( x in AtomSet X iff for z being Element of X holds ((x \ z) `) ` = x \ z )

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

then ((x \ (0. X)) `) ` = x \ (0. X) ;

then (x `) ` = x \ (0. X) by Th2;

then (x `) ` = x by Th2;

hence x in AtomSet X by Th29; :: thesis: verum

( x in AtomSet X iff for z being Element of X holds ((x \ z) `) ` = x \ z )

let x be Element of X; :: thesis: ( x in AtomSet X iff for z being Element of X holds ((x \ z) `) ` = x \ z )

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

proof

assume
for z being Element of X holds ((x \ z) `) ` = x \ z
; :: thesis: x in AtomSet X
assume A1:
x in AtomSet X
; :: thesis: for z being Element of X holds ((x \ z) `) ` = x \ z

let z be Element of X; :: thesis: ((x \ z) `) ` = x \ z

A2: (z \ (z \ x)) \ x = 0. X by Th1;

ex x1 being Element of X st

( x = x1 & x1 is atom ) by A1;

then z \ (z \ x) = x by A2;

then ((x \ z) `) ` = (((z \ z) \ (z \ x)) `) ` by Th7;

then ((x \ z) `) ` = (((z \ x) `) `) ` by Def5;

then ((x \ z) `) ` = (z \ x) ` by Th8;

hence ((x \ z) `) ` = x \ z by A1, Th30; :: thesis: verum

end;let z be Element of X; :: thesis: ((x \ z) `) ` = x \ z

A2: (z \ (z \ x)) \ x = 0. X by Th1;

ex x1 being Element of X st

( x = x1 & x1 is atom ) by A1;

then z \ (z \ x) = x by A2;

then ((x \ z) `) ` = (((z \ z) \ (z \ x)) `) ` by Th7;

then ((x \ z) `) ` = (((z \ x) `) `) ` by Def5;

then ((x \ z) `) ` = (z \ x) ` by Th8;

hence ((x \ z) `) ` = x \ z by A1, Th30; :: thesis: verum

then ((x \ (0. X)) `) ` = x \ (0. X) ;

then (x `) ` = x \ (0. X) by Th2;

then (x `) ` = x by Th2;

hence x in AtomSet X by Th29; :: thesis: verum