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 )

x ` = y ` ) implies x ` is minimal ) :: thesis: verum

( 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

thus
( ( for y being Element of X st y <= x holds
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;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

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

end;x ` = y ` ; :: thesis: x ` is minimal

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

xx = x `

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