let X be BCI-algebra; :: thesis: for x being Element of X holds
( x ` is minimal iff for y, z being Element of X holds (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `) )
let x be Element of X; :: thesis: ( x ` is minimal iff for y, z being Element of X holds (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `) )
thus ( x ` is minimal implies for y, z being Element of X holds (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `) ) :: thesis: ( ( for y, z being Element of X holds (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `) ) implies x ` is minimal )

proof

assume A1: x ` is minimal ; :: thesis: for y, z being Element of X holds (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `)
let y, z be Element of X; :: thesis: (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `)
((y `) \ (x \ y)) \ (x `) = 0. X by BCIALG_1:def 3;
then A2: (y `) \ (x \ y) <= x ` ;
(((x \ z) \ (y \ z)) `) ` = (((x \ z) `) \ ((y \ z) `)) ` by BCIALG_1:9
.= (((x `) \ (z `)) \ ((y \ z) `)) ` by BCIALG_1:9 ;
then (((x \ z) \ (y \ z)) `) ` = ((((y `) \ (x \ y)) \ (z `)) \ ((y \ z) `)) ` by A1, A2
.= ((((y `) \ (z `)) \ (x \ y)) \ ((y \ z) `)) ` by BCIALG_1:7
.= ((((y \ z) `) \ (x \ y)) \ ((y \ z) `)) ` by BCIALG_1:9
.= ((((y \ z) `) \ ((y \ z) `)) \ (x \ y)) ` by BCIALG_1:7
.= ((x \ y) `) ` by BCIALG_1:def 5
.= ((x `) \ (y `)) ` by BCIALG_1:9
.= (((y `) `) \ x) ` by BCIALG_1:7
.= (((y `) `) `) \ (x `) by BCIALG_1:9
.= (y `) \ (x `) by BCIALG_1:8 ;
hence (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `) ; :: thesis: verum

end;

thus ( ( for y, z being Element of X holds (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `) ) implies x ` is minimal ) :: thesis: verum

proof

assume A3: for y, z being Element of X holds (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `) ; :: thesis: x ` is minimal

now :: thesis: for x1 being Element of X st x1 <= x ` holds
x1 = x `

let x1 be Element of X; :: thesis: ( x1 <= x ` implies x1 = x ` )
assume x1 <= x ` ; :: thesis: x1 = x `
then A4: x1 \ (x `) = 0. X ;
then ((x1 `) \ (x `)) \ ((x1 `) \ x1) = 0. X by BCIALG_1:4;
then ((((x \ (0. X)) \ (x1 \ (0. X))) `) `) \ ((x1 `) \ x1) = 0. X by A3;
then (((x1 `) \ x1) `) \ (((x \ (0. X)) \ (x1 \ (0. X))) `) = 0. X by BCIALG_1:7;
then (((x1 `) \ x1) `) \ ((x \ (x1 \ (0. X))) `) = 0. X by BCIALG_1:2;
then (((x1 `) \ x1) `) \ ((x \ x1) `) = 0. X by BCIALG_1:2;
then (((x1 `) `) \ (x1 `)) \ ((x \ x1) `) = 0. X by BCIALG_1:9;
then (((x1 `) `) \ (x1 `)) \ ((x `) \ (x1 `)) = 0. X by BCIALG_1:9;
then (((x1 `) `) \ (x `)) ` = 0. X by BCIALG_1:def 3;
then (((x1 `) `) `) \ ((x `) `) = 0. X by BCIALG_1:9;
then (x1 `) \ ((x `) `) = 0. X by BCIALG_1:8;
then (((x `) `) `) \ x1 = 0. X by BCIALG_1:7;
then (x `) \ x1 = 0. X by BCIALG_1:8;
hence x1 = x ` by A4, BCIALG_1:def 7; :: thesis: verum

end;

hence x ` is minimal by Lm1; :: thesis: verum

end;