let X be BCI-algebra; :: thesis: for a being Element of X holds
( a is minimal iff for x being Element of X holds a \ x = (x `) \ (a `) )
let a be Element of X; :: thesis: ( a is minimal iff for x being Element of X holds a \ x = (x `) \ (a `) )
thus ( a is minimal implies for x being Element of X holds a \ x = (x `) \ (a `) ) :: thesis: ( ( for x being Element of X holds a \ x = (x `) \ (a `) ) implies a is minimal )
proof
assume A1: a is minimal ; :: thesis: for x being Element of X holds a \ x = (x `) \ (a `)
let x be Element of X; :: thesis: a \ x = (x `) \ (a `)
(x \ (x \ a)) \ a = 0. X by BCIALG_1:1;
then x \ (x \ a) <= a ;
then A2: (a \ x) \ ((x `) \ (a `)) = ((x \ (x \ a)) \ x) \ ((x `) \ (a `)) by A1
.= ((x \ x) \ (x \ a)) \ ((x `) \ (a `)) by BCIALG_1:7
.= ((x \ a) `) \ ((x `) \ (a `)) by BCIALG_1:def 5
.= ((x \ a) `) \ ((x \ a) `) by BCIALG_1:9
.= 0. X by BCIALG_1:def 5 ;
((x `) \ (a `)) \ (a \ x) = 0. X by BCIALG_1:1;
hence a \ x = (x `) \ (a `) by A2, BCIALG_1:def 7; :: thesis: verum
end;
thus ( ( for x being Element of X holds a \ x = (x `) \ (a `) ) implies a is minimal ) :: thesis: verum
proof
assume A3: for x being Element of X holds a \ x = (x `) \ (a `) ; :: thesis: a is minimal
now :: thesis: for x being Element of X st x <= a holds
a = x
let x be Element of X; :: thesis: ( x <= a implies a = x )
assume x <= a ; :: thesis: a = x
then A4: x \ a = 0. X ;
a \ x = (x `) \ (a `) by A3;
then a \ x = (0. X) ` by A4, BCIALG_1:9;
then a \ x = 0. X by BCIALG_1:def 5;
hence a = x by A4, BCIALG_1:def 7; :: thesis: verum
end;
hence a is minimal by Lm1; :: thesis: verum
end;