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

proof

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

end;

thus ( ( for y being Element of X st y <= x holds
x ` = y ` ) implies x ` is minimal ) :: thesis: verum

proof

assume A2: for y being Element of X st y <= x holds
x ` = y ` ; :: thesis: x ` is minimal

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

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

end;

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

end;