let i, j, m, n be Nat; :: thesis: for X being BCK-algebra of i,j,m,n st i <= m & j <= n holds

X is BCK-algebra of i,j,i,j

let X be BCK-algebra of i,j,m,n; :: thesis: ( i <= m & j <= n implies X is BCK-algebra of i,j,i,j )

assume that

A1: i <= m and

A2: j <= n ; :: thesis: X is BCK-algebra of i,j,i,j

A3: for x, y being Element of X holds Polynom (i,j,x,y) <= Polynom (i,j,y,x)

X is BCK-algebra of i,j,i,j

let X be BCK-algebra of i,j,m,n; :: thesis: ( i <= m & j <= n implies X is BCK-algebra of i,j,i,j )

assume that

A1: i <= m and

A2: j <= n ; :: thesis: X is BCK-algebra of i,j,i,j

A3: for x, y being Element of X holds Polynom (i,j,x,y) <= Polynom (i,j,y,x)

proof

for x, y being Element of X holds Polynom (i,j,y,x) = Polynom (i,j,x,y)
let x, y be Element of X; :: thesis: Polynom (i,j,x,y) <= Polynom (i,j,y,x)

i + 1 <= m + 1 by A1, XREAL_1:6;

then A4: (((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power n <= (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power n by Th5, BCIALG_2:19;

( Polynom (i,j,x,y) = Polynom (m,n,y,x) & (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power n <= (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power j ) by A2, Def3, Th5;

hence Polynom (i,j,x,y) <= Polynom (i,j,y,x) by A4, Th1; :: thesis: verum

end;i + 1 <= m + 1 by A1, XREAL_1:6;

then A4: (((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power n <= (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power n by Th5, BCIALG_2:19;

( Polynom (i,j,x,y) = Polynom (m,n,y,x) & (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power n <= (((y,(y \ x)) to_power (i + 1)),(x \ y)) to_power j ) by A2, Def3, Th5;

hence Polynom (i,j,x,y) <= Polynom (i,j,y,x) by A4, Th1; :: thesis: verum

proof

hence
X is BCK-algebra of i,j,i,j
by Def3; :: thesis: verum
let x, y be Element of X; :: thesis: Polynom (i,j,y,x) = Polynom (i,j,x,y)

Polynom (i,j,x,y) <= Polynom (i,j,y,x) by A3;

then A5: (Polynom (i,j,x,y)) \ (Polynom (i,j,y,x)) = 0. X ;

Polynom (i,j,y,x) <= Polynom (i,j,x,y) by A3;

then (Polynom (i,j,y,x)) \ (Polynom (i,j,x,y)) = 0. X ;

hence Polynom (i,j,y,x) = Polynom (i,j,x,y) by A5, BCIALG_1:def 7; :: thesis: verum

end;Polynom (i,j,x,y) <= Polynom (i,j,y,x) by A3;

then A5: (Polynom (i,j,x,y)) \ (Polynom (i,j,y,x)) = 0. X ;

Polynom (i,j,y,x) <= Polynom (i,j,x,y) by A3;

then (Polynom (i,j,y,x)) \ (Polynom (i,j,x,y)) = 0. X ;

hence Polynom (i,j,y,x) = Polynom (i,j,x,y) by A5, BCIALG_1:def 7; :: thesis: verum