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 ` )
A2: (((x \ z) \ (y \ z)) ` ) ` = (((x \ z) ` ) \ ((y \ z) ` )) ` by BCIALG_1:9
.= (((x ` ) \ (z ` )) \ ((y \ z) ` )) ` by BCIALG_1:9 ;
((y ` ) \ (x \ y)) \ (x ` ) = 0. X by BCIALG_1:def 3;
then (y ` ) \ (x \ y) <= x ` by BCIALG_1:def 11;
then (((x \ z) \ (y \ z)) ` ) ` = ((((y ` ) \ (x \ y)) \ (z ` )) \ ((y \ z) ` )) ` by A1, A2, Lm1
.= ((((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

let x1 be Element of X; :: thesis: ( x1 <= x ` implies x1 = x ` )
assume x1 <= x ` ; :: thesis: x1 = x `
then A4: x1 \ (x ` ) = 0. X by BCIALG_1:def 11;
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;