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

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

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

hence x in AtomSet X ; :: thesis: verum

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

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

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

proof

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

then A1: ex x1 being Element of X st

( x = x1 & x1 is atom ) ;

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

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

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

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

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

hence (z `) \ (x `) = x \ z by Th9; :: thesis: verum

end;then A1: ex x1 being Element of X st

( x = x1 & x1 is atom ) ;

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

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

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

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

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

hence (z `) \ (x `) = x \ z by Th9; :: thesis: verum

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

z = x

then
x is atom
;z = x

let z be Element of X; :: thesis: ( z \ x = 0. X implies z = x )

assume A3: z \ x = 0. X ; :: thesis: z = x

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

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

then x \ z = 0. X by A2;

hence z = x by A3, Def7; :: thesis: verum

end;assume A3: z \ x = 0. X ; :: thesis: z = x

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

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

then x \ z = 0. X by A2;

hence z = x by A3, Def7; :: thesis: verum

hence x in AtomSet X ; :: thesis: verum