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 )

A1: ( ( for z being Element of X holds (z `) \ (x `) = x \ z ) implies for z being Element of X holds (z \ x) ` = x \ z )

( 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 )

A1: ( ( for z being Element of X holds (z `) \ (x `) = x \ z ) implies for z being Element of X holds (z \ x) ` = x \ z )

proof

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

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

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

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

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

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

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

proof

hence
( x in AtomSet X iff for z being Element of X holds (z \ x) ` = x \ z )
by A1, Th28; :: thesis: verum
assume A3:
for z being Element of X holds (z \ x) ` = x \ z
; :: thesis: for z being Element of X holds (z `) \ (x `) = x \ z

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

(z \ x) ` = x \ z by A3;

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

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

(z \ x) ` = x \ z by A3;

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