let X be BCI-algebra; :: thesis: for x being Element of X holds

( x in AtomSet X iff (x `) ` = x )

let x be Element of X; :: thesis: ( x in AtomSet X iff (x `) ` = x )

thus ( x in AtomSet X implies (x `) ` = x ) :: thesis: ( (x `) ` = x implies x in AtomSet X )

hence x in AtomSet X ; :: thesis: verum

( x in AtomSet X iff (x `) ` = x )

let x be Element of X; :: thesis: ( x in AtomSet X iff (x `) ` = x )

thus ( x in AtomSet X implies (x `) ` = x ) :: thesis: ( (x `) ` = x implies x in AtomSet X )

proof

assume A1:
(x `) ` = x
; :: thesis: x in AtomSet X
assume
x in AtomSet X
; :: thesis: (x `) ` = x

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

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

hence (x `) ` = x by Def5; :: thesis: verum

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

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

hence (x `) ` = x by Def5; :: 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 A2: z \ x = 0. X ; :: thesis: z = x

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

then 0. X = x \ z by Def3;

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

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

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

then 0. X = x \ z by Def3;

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

hence x in AtomSet X ; :: thesis: verum