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 )

( 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

thus
( ( for y, z being Element of X holds (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `) ) implies x ` is minimal )
:: thesis: verum
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;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

proof

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

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

x1 = x `

hence
x ` is minimal
by Lm1; :: thesis: verumx1 = 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;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