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

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

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

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

then for u being Element of X holds ((x \ u) `) ` = x \ u ;

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

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

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

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

proof

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

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

x \ u = ((x \ u) `) ` by A1, Th31

.= ((z \ z) \ (x \ u)) ` by Def5

.= ((z \ (x \ u)) \ z) ` by Th7

.= ((z \ (x \ u)) `) \ (z `) by Th9 ;

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

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

hence z \ (z \ (x \ u)) = x \ u by A2, Def7; :: thesis: verum

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

x \ u = ((x \ u) `) ` by A1, Th31

.= ((z \ z) \ (x \ u)) ` by Def5

.= ((z \ (x \ u)) \ z) ` by Th7

.= ((z \ (x \ u)) `) \ (z `) by Th9 ;

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

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

hence z \ (z \ (x \ u)) = x \ u by A2, Def7; :: thesis: verum

then for u being Element of X holds ((x \ u) `) ` = x \ u ;

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