:: BCIALG_5 semantic presentation

REAL is non empty V33() set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K6(REAL)

K6(REAL) is set

NAT is non empty epsilon-transitive epsilon-connected ordinal set

K6(NAT) is set

{} is set

the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() ext-real non positive non negative set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() ext-real non positive non negative set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

i is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of i is non empty set

j is Element of the carrier of i

m is Element of the carrier of i

j \ m is Element of the carrier of i

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(j,(j \ m)) to_power (n + 1) is Element of the carrier of i

m \ j is Element of the carrier of i

X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

(((j,(j \ m)) to_power (n + 1)),(m \ j)) to_power X is Element of the carrier of i

i is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of i is non empty set

j is Element of the carrier of i

m is Element of the carrier of i

n is Element of the carrier of i

j \ m is Element of the carrier of i

0. i is V49(i) minimal positive V92(i) Element of the carrier of i

m \ n is Element of the carrier of i

j \ n is Element of the carrier of i

i is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of i is non empty set

j is Element of the carrier of i

m is Element of the carrier of i

j \ m is Element of the carrier of i

0. i is V49(i) minimal positive V92(i) Element of the carrier of i

m \ j is Element of the carrier of i

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

j is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of j is non empty set

m is Element of the carrier of j

n is Element of the carrier of j

m \ n is Element of the carrier of j

(m,n) to_power (i + 1) is Element of the carrier of j

(m,n) to_power i is Element of the carrier of j

((m,n) to_power i) \ n is Element of the carrier of j

(((m,n) to_power i) \ n) \ ((m,n) to_power i) is Element of the carrier of j

((m,n) to_power i) \ ((m,n) to_power i) is Element of the carrier of j

(((m,n) to_power i) \ ((m,n) to_power i)) \ n is Element of the carrier of j

n ` is Element of the carrier of j

0. j is V49(j) minimal positive V92(j) Element of the carrier of j

(0. j) \ n is Element of the carrier of j

(m \ n) \ m is Element of the carrier of j

m \ m is Element of the carrier of j

(m \ m) \ n is Element of the carrier of j

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of j is non empty set

0. j is V49(j) minimal positive V92(j) Element of the carrier of j

m is Element of the carrier of j

((0. j),m) to_power i is Element of the carrier of j

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

((0. j),m) to_power n is Element of the carrier of j

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

((0. j),m) to_power (n + 1) is Element of the carrier of j

m ` is Element of the carrier of j

(0. j) \ m is Element of the carrier of j

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

((0. j),m) to_power n is Element of the carrier of j

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

((0. j),m) to_power (n + 1) is Element of the carrier of j

((0. j),m) to_power 0 is Element of the carrier of j

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of m is non empty set

n is Element of the carrier of m

X is Element of the carrier of m

(n,X) to_power i is Element of the carrier of m

(n,X) to_power j is Element of the carrier of m

i - j is V11() V12() ext-real Element of REAL

X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

(n,X) to_power X is Element of the carrier of m

((n,X) to_power X) \ n is Element of the carrier of m

n \ n is Element of the carrier of m

((n \ n),X) to_power X is Element of the carrier of m

0. m is V49(m) minimal positive V92(m) Element of the carrier of m

((0. m),X) to_power X is Element of the carrier of m

(((n,X) to_power X),X) to_power j is Element of the carrier of m

X + j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

(n,X) to_power (X + j) is Element of the carrier of m

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCIStr_0

the carrier of m is non empty set

n is Element of the carrier of m

X is Element of the carrier of m

(n,X) to_power j is Element of the carrier of m

(n,X) to_power i is Element of the carrier of m

i - j is V11() V12() ext-real Element of REAL

j - j is V11() V12() ext-real Element of REAL

1 + j is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(i - j) + j is V11() V12() ext-real Element of REAL

j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(n,X) to_power (j + 1) is Element of the carrier of m

X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

(n,X) to_power X is Element of the carrier of m

X - j is V11() V12() ext-real Element of REAL

x is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

(((n,X) to_power j),X) to_power x is Element of the carrier of m

y is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

(((n,X) to_power j),X) to_power y is Element of the carrier of m

y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(((n,X) to_power j),X) to_power (y + 1) is Element of the carrier of m

((((n,X) to_power j),X) to_power y) \ X is Element of the carrier of m

((n,X) to_power j) \ X is Element of the carrier of m

((((n,X) to_power j) \ X),X) to_power y is Element of the carrier of m

(((n,X) to_power (j + 1)),X) to_power y is Element of the carrier of m

y is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

(((n,X) to_power j),X) to_power y is Element of the carrier of m

y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(((n,X) to_power j),X) to_power (y + 1) is Element of the carrier of m

(((n,X) to_power j),X) to_power 0 is Element of the carrier of m

j + x is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

(n,X) to_power (j + x) is Element of the carrier of m

X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

(n,X) to_power X is Element of the carrier of m

i is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of i is non empty set

j is Element of the carrier of i

m is Element of the carrier of i

(i,j,m,0,0) is Element of the carrier of i

j \ m is Element of the carrier of i

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(j,(j \ m)) to_power (0 + 1) is Element of the carrier of i

m \ j is Element of the carrier of i

(((j,(j \ m)) to_power (0 + 1)),(m \ j)) to_power 0 is Element of the carrier of i

j \ (j \ m) is Element of the carrier of i

i is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of i is non empty set

j is Element of the carrier of i

m is Element of the carrier of i

(i,j,m,0,0) is Element of the carrier of i

j \ m is Element of the carrier of i

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(j,(j \ m)) to_power (0 + 1) is Element of the carrier of i

m \ j is Element of the carrier of i

(((j,(j \ m)) to_power (0 + 1)),(m \ j)) to_power 0 is Element of the carrier of i

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

((i,j,m,0,0),(j \ m)) to_power n is Element of the carrier of i

X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

(i,j,m,n,X) is Element of the carrier of i

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(j,(j \ m)) to_power (n + 1) is Element of the carrier of i

(((j,(j \ m)) to_power (n + 1)),(m \ j)) to_power X is Element of the carrier of i

((((i,j,m,0,0),(j \ m)) to_power n),(m \ j)) to_power X is Element of the carrier of i

j \ (j \ m) is Element of the carrier of i

((j \ (j \ m)),(j \ m)) to_power n is Element of the carrier of i

(j,(j \ m)) to_power n is Element of the carrier of i

((j,(j \ m)) to_power n) \ (j \ m) is Element of the carrier of i

i is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of i is non empty set

j is Element of the carrier of i

m is Element of the carrier of i

j \ m is Element of the carrier of i

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

(i,j,m,(n + 1),X) is Element of the carrier of i

(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(j,(j \ m)) to_power ((n + 1) + 1) is Element of the carrier of i

m \ j is Element of the carrier of i

(((j,(j \ m)) to_power ((n + 1) + 1)),(m \ j)) to_power X is Element of the carrier of i

(i,j,m,n,X) is Element of the carrier of i

(j,(j \ m)) to_power (n + 1) is Element of the carrier of i

(((j,(j \ m)) to_power (n + 1)),(m \ j)) to_power X is Element of the carrier of i

(i,j,m,n,X) \ (j \ m) is Element of the carrier of i

(j,(m \ j)) to_power X is Element of the carrier of i

(((j,(m \ j)) to_power X),(j \ m)) to_power ((n + 1) + 1) is Element of the carrier of i

(((j,(m \ j)) to_power X),(j \ m)) to_power (n + 1) is Element of the carrier of i

((((j,(m \ j)) to_power X),(j \ m)) to_power (n + 1)) \ (j \ m) is Element of the carrier of i

((((j,(j \ m)) to_power (n + 1)),(m \ j)) to_power X) \ (j \ m) is Element of the carrier of i

i is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of i is non empty set

j is Element of the carrier of i

m is Element of the carrier of i

m \ j is Element of the carrier of i

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(i,j,m,n,(X + 1)) is Element of the carrier of i

j \ m is Element of the carrier of i

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(j,(j \ m)) to_power (n + 1) is Element of the carrier of i

(((j,(j \ m)) to_power (n + 1)),(m \ j)) to_power (X + 1) is Element of the carrier of i

(i,j,m,n,X) is Element of the carrier of i

(((j,(j \ m)) to_power (n + 1)),(m \ j)) to_power X is Element of the carrier of i

(i,j,m,n,X) \ (m \ j) is Element of the carrier of i

K7(NAT, the carrier of i) is set

K6(K7(NAT, the carrier of i)) is set

X is V21() V30( NAT , the carrier of i) Element of K6(K7(NAT, the carrier of i))

X . (X + 1) is Element of the carrier of i

X . 0 is Element of the carrier of i

x is V21() V30( NAT , the carrier of i) Element of K6(K7(NAT, the carrier of i))

x . X is Element of the carrier of i

x . 0 is Element of the carrier of i

y is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X . y is Element of the carrier of i

x . y is Element of the carrier of i

y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

X . (y + 1) is Element of the carrier of i

(X . y) \ (m \ j) is Element of the carrier of i

x . (y + 1) is Element of the carrier of i

y is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X . y is Element of the carrier of i

x . y is Element of the carrier of i

y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

X . (y + 1) is Element of the carrier of i

x . (y + 1) is Element of the carrier of i

X . X is Element of the carrier of i

i is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of i is non empty set

j is Element of the carrier of i

m is Element of the carrier of i

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(i,j,m,(n + 1),(n + 1)) is Element of the carrier of i

j \ m is Element of the carrier of i

(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(j,(j \ m)) to_power ((n + 1) + 1) is Element of the carrier of i

m \ j is Element of the carrier of i

(((j,(j \ m)) to_power ((n + 1) + 1)),(m \ j)) to_power (n + 1) is Element of the carrier of i

(i,m,j,n,(n + 1)) is Element of the carrier of i

(m,(m \ j)) to_power (n + 1) is Element of the carrier of i

(((m,(m \ j)) to_power (n + 1)),(j \ m)) to_power (n + 1) is Element of the carrier of i

(j \ m) \ (j \ m) is Element of the carrier of i

0. i is V49(i) minimal positive V92(i) Element of the carrier of i

j \ (j \ m) is Element of the carrier of i

(j \ (j \ m)) \ m is Element of the carrier of i

((j \ (j \ m)),(m \ j)) to_power (n + 1) is Element of the carrier of i

((((j \ (j \ m)),(m \ j)) to_power (n + 1)),(j \ m)) to_power (n + 1) is Element of the carrier of i

((j \ (j \ m)),(j \ m)) to_power (n + 1) is Element of the carrier of i

((((j \ (j \ m)),(j \ m)) to_power (n + 1)),(m \ j)) to_power (n + 1) is Element of the carrier of i

(j,(j \ m)) to_power 1 is Element of the carrier of i

(((j,(j \ m)) to_power 1),(j \ m)) to_power (n + 1) is Element of the carrier of i

(((((j,(j \ m)) to_power 1),(j \ m)) to_power (n + 1)),(m \ j)) to_power (n + 1) is Element of the carrier of i

i is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of i is non empty set

j is Element of the carrier of i

m is Element of the carrier of i

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(i,j,m,n,(n + 1)) is Element of the carrier of i

j \ m is Element of the carrier of i

(j,(j \ m)) to_power (n + 1) is Element of the carrier of i

m \ j is Element of the carrier of i

(((j,(j \ m)) to_power (n + 1)),(m \ j)) to_power (n + 1) is Element of the carrier of i

(i,m,j,n,n) is Element of the carrier of i

(m,(m \ j)) to_power (n + 1) is Element of the carrier of i

(((m,(m \ j)) to_power (n + 1)),(j \ m)) to_power n is Element of the carrier of i

(j \ m) \ (j \ m) is Element of the carrier of i

0. i is V49(i) minimal positive V92(i) Element of the carrier of i

j \ (j \ m) is Element of the carrier of i

(j \ (j \ m)) \ m is Element of the carrier of i

((j \ (j \ m)),(j \ m)) to_power n is Element of the carrier of i

(m,(j \ m)) to_power n is Element of the carrier of i

((((j \ (j \ m)),(j \ m)) to_power n),(m \ j)) to_power (n + 1) is Element of the carrier of i

(((m,(j \ m)) to_power n),(m \ j)) to_power (n + 1) is Element of the carrier of i

(j,(j \ m)) to_power 1 is Element of the carrier of i

(((j,(j \ m)) to_power 1),(j \ m)) to_power n is Element of the carrier of i

(((((j,(j \ m)) to_power 1),(j \ m)) to_power n),(m \ j)) to_power (n + 1) is Element of the carrier of i

BCI-EXAMPLE is non empty V47() V48() 1 -element strict being_B being_C being_I being_BCI-4 being_BCK-5 associative positive-implicative weakly-positive-implicative implicative weakly-implicative p-Semisimple alternative commutative BCI-commutative BCI-weakly-commutative V99() Iseki_extension BCK-positive-implicative BCK-implicative BCIStr_0

the carrier of BCI-EXAMPLE is non empty V2() V33() set

i is Element of the carrier of BCI-EXAMPLE

j is Element of the carrier of BCI-EXAMPLE

(BCI-EXAMPLE,i,j,0,0) is Element of the carrier of BCI-EXAMPLE

i \ j is Element of the carrier of BCI-EXAMPLE

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(i,(i \ j)) to_power (0 + 1) is Element of the carrier of BCI-EXAMPLE

j \ i is Element of the carrier of BCI-EXAMPLE

(((i,(i \ j)) to_power (0 + 1)),(j \ i)) to_power 0 is Element of the carrier of BCI-EXAMPLE

(BCI-EXAMPLE,j,i,0,0) is Element of the carrier of BCI-EXAMPLE

(j,(j \ i)) to_power (0 + 1) is Element of the carrier of BCI-EXAMPLE

(((j,(j \ i)) to_power (0 + 1)),(i \ j)) to_power 0 is Element of the carrier of BCI-EXAMPLE

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

the carrier of BCI-EXAMPLE is non empty V2() V33() set

X is Element of the carrier of BCI-EXAMPLE

X is Element of the carrier of BCI-EXAMPLE

(BCI-EXAMPLE,X,X,i,j) is Element of the carrier of BCI-EXAMPLE

X \ X is Element of the carrier of BCI-EXAMPLE

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,(X \ X)) to_power (i + 1) is Element of the carrier of BCI-EXAMPLE

X \ X is Element of the carrier of BCI-EXAMPLE

(((X,(X \ X)) to_power (i + 1)),(X \ X)) to_power j is Element of the carrier of BCI-EXAMPLE

(BCI-EXAMPLE,X,X,m,n) is Element of the carrier of BCI-EXAMPLE

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,(X \ X)) to_power (m + 1) is Element of the carrier of BCI-EXAMPLE

(((X,(X \ X)) to_power (m + 1)),(X \ X)) to_power n is Element of the carrier of BCI-EXAMPLE

i is non empty being_B being_C being_I being_BCI-4 BCIStr_0

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

the carrier of i is non empty set

X is Element of the carrier of i

x is Element of the carrier of i

(i,X,x,n,X) is Element of the carrier of i

X \ x is Element of the carrier of i

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,(X \ x)) to_power (n + 1) is Element of the carrier of i

x \ X is Element of the carrier of i

(((X,(X \ x)) to_power (n + 1)),(x \ X)) to_power X is Element of the carrier of i

(i,x,X,j,m) is Element of the carrier of i

j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ X)) to_power (j + 1) is Element of the carrier of i

(((x,(x \ X)) to_power (j + 1)),(X \ x)) to_power m is Element of the carrier of i

the carrier of i is non empty set

x is Element of the carrier of i

X is Element of the carrier of i

(i,x,X,n,X) is Element of the carrier of i

x \ X is Element of the carrier of i

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ X)) to_power (n + 1) is Element of the carrier of i

X \ x is Element of the carrier of i

(((x,(x \ X)) to_power (n + 1)),(X \ x)) to_power X is Element of the carrier of i

(i,X,x,j,m) is Element of the carrier of i

j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,(X \ x)) to_power (j + 1) is Element of the carrier of i

(((X,(X \ x)) to_power (j + 1)),(x \ X)) to_power m is Element of the carrier of i

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is non empty being_B being_C being_I being_BCI-4 (i,j,m,n)

X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

i + X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n + X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

the carrier of X is non empty set

x is Element of the carrier of X

y is Element of the carrier of X

(X,x,y,(i + X),j) is Element of the carrier of X

x \ y is Element of the carrier of X

(i + X) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ y)) to_power ((i + X) + 1) is Element of the carrier of X

y \ x is Element of the carrier of X

(((x,(x \ y)) to_power ((i + X) + 1)),(y \ x)) to_power j is Element of the carrier of X

(X,y,x,m,(n + X)) is Element of the carrier of X

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(y,(y \ x)) to_power (m + 1) is Element of the carrier of X

(((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power (n + X) is Element of the carrier of X

(X,y,x,m,n) is Element of the carrier of X

(((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power n is Element of the carrier of X

((X,y,x,m,n),(x \ y)) to_power X is Element of the carrier of X

(X,x,y,i,j) is Element of the carrier of X

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ y)) to_power (i + 1) is Element of the carrier of X

(((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power j is Element of the carrier of X

((X,x,y,i,j),(x \ y)) to_power X is Element of the carrier of X

(((x,(x \ y)) to_power (i + 1)),(x \ y)) to_power X is Element of the carrier of X

(((((x,(x \ y)) to_power (i + 1)),(x \ y)) to_power X),(y \ x)) to_power j is Element of the carrier of X

(i + 1) + X is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ y)) to_power ((i + 1) + X) is Element of the carrier of X

(((x,(x \ y)) to_power ((i + 1) + X)),(y \ x)) to_power j is Element of the carrier of X

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is non empty being_B being_C being_I being_BCI-4 (i,j,m,n)

X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j + X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m + X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

the carrier of X is non empty set

x is Element of the carrier of X

y is Element of the carrier of X

(X,x,y,i,(j + X)) is Element of the carrier of X

x \ y is Element of the carrier of X

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ y)) to_power (i + 1) is Element of the carrier of X

y \ x is Element of the carrier of X

(((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power (j + X) is Element of the carrier of X

(X,y,x,(m + X),n) is Element of the carrier of X

(m + X) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(y,(y \ x)) to_power ((m + X) + 1) is Element of the carrier of X

(((y,(y \ x)) to_power ((m + X) + 1)),(x \ y)) to_power n is Element of the carrier of X

(X,y,x,m,n) is Element of the carrier of X

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(y,(y \ x)) to_power (m + 1) is Element of the carrier of X

(((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power n is Element of the carrier of X

((X,y,x,m,n),(y \ x)) to_power X is Element of the carrier of X

(((y,(y \ x)) to_power (m + 1)),(y \ x)) to_power X is Element of the carrier of X

(((((y,(y \ x)) to_power (m + 1)),(y \ x)) to_power X),(x \ y)) to_power n is Element of the carrier of X

(m + 1) + X is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(y,(y \ x)) to_power ((m + 1) + X) is Element of the carrier of X

(((y,(y \ x)) to_power ((m + 1) + X)),(x \ y)) to_power n is Element of the carrier of X

(X,x,y,i,j) is Element of the carrier of X

(((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power j is Element of the carrier of X

((X,x,y,i,j),(y \ x)) to_power X is Element of the carrier of X

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

the carrier of BCI-EXAMPLE is non empty V2() V33() set

X is Element of the carrier of BCI-EXAMPLE

X is Element of the carrier of BCI-EXAMPLE

(BCI-EXAMPLE,X,X,i,j) is Element of the carrier of BCI-EXAMPLE

X \ X is Element of the carrier of BCI-EXAMPLE

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,(X \ X)) to_power (i + 1) is Element of the carrier of BCI-EXAMPLE

X \ X is Element of the carrier of BCI-EXAMPLE

(((X,(X \ X)) to_power (i + 1)),(X \ X)) to_power j is Element of the carrier of BCI-EXAMPLE

(BCI-EXAMPLE,X,X,m,n) is Element of the carrier of BCI-EXAMPLE

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,(X \ X)) to_power (m + 1) is Element of the carrier of BCI-EXAMPLE

(((X,(X \ X)) to_power (m + 1)),(X \ X)) to_power n is Element of the carrier of BCI-EXAMPLE

X is non empty being_B being_C being_I being_BCI-4 (i,j,m,n)

i is non empty being_B being_C being_I being_BCI-4 BCIStr_0

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

the carrier of i is non empty set

X is Element of the carrier of i

x is Element of the carrier of i

(i,X,x,n,X) is Element of the carrier of i

X \ x is Element of the carrier of i

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,(X \ x)) to_power (n + 1) is Element of the carrier of i

x \ X is Element of the carrier of i

(((X,(X \ x)) to_power (n + 1)),(x \ X)) to_power X is Element of the carrier of i

(i,x,X,j,m) is Element of the carrier of i

j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ X)) to_power (j + 1) is Element of the carrier of i

(((x,(x \ X)) to_power (j + 1)),(X \ x)) to_power m is Element of the carrier of i

the carrier of i is non empty set

x is Element of the carrier of i

X is Element of the carrier of i

(i,x,X,n,X) is Element of the carrier of i

x \ X is Element of the carrier of i

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ X)) to_power (n + 1) is Element of the carrier of i

X \ x is Element of the carrier of i

(((x,(x \ X)) to_power (n + 1)),(X \ x)) to_power X is Element of the carrier of i

(i,X,x,j,m) is Element of the carrier of i

j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,(X \ x)) to_power (j + 1) is Element of the carrier of i

(((X,(X \ x)) to_power (j + 1)),(x \ X)) to_power m is Element of the carrier of i

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)

X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

i + X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n + X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

the carrier of X is non empty set

x is Element of the carrier of X

y is Element of the carrier of X

(X,x,y,(i + X),j) is Element of the carrier of X

x \ y is Element of the carrier of X

(i + X) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ y)) to_power ((i + X) + 1) is Element of the carrier of X

y \ x is Element of the carrier of X

(((x,(x \ y)) to_power ((i + X) + 1)),(y \ x)) to_power j is Element of the carrier of X

(X,y,x,m,(n + X)) is Element of the carrier of X

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(y,(y \ x)) to_power (m + 1) is Element of the carrier of X

(((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power (n + X) is Element of the carrier of X

(X,y,x,m,n) is Element of the carrier of X

(((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power n is Element of the carrier of X

((X,y,x,m,n),(x \ y)) to_power X is Element of the carrier of X

(X,x,y,i,j) is Element of the carrier of X

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ y)) to_power (i + 1) is Element of the carrier of X

(((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power j is Element of the carrier of X

((X,x,y,i,j),(x \ y)) to_power X is Element of the carrier of X

(((x,(x \ y)) to_power (i + 1)),(x \ y)) to_power X is Element of the carrier of X

(((((x,(x \ y)) to_power (i + 1)),(x \ y)) to_power X),(y \ x)) to_power j is Element of the carrier of X

(i + 1) + X is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ y)) to_power ((i + 1) + X) is Element of the carrier of X

(((x,(x \ y)) to_power ((i + 1) + X)),(y \ x)) to_power j is Element of the carrier of X

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)

X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j + X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m + X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

the carrier of X is non empty set

x is Element of the carrier of X

y is Element of the carrier of X

(X,x,y,i,(j + X)) is Element of the carrier of X

x \ y is Element of the carrier of X

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ y)) to_power (i + 1) is Element of the carrier of X

y \ x is Element of the carrier of X

(((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power (j + X) is Element of the carrier of X

(X,y,x,(m + X),n) is Element of the carrier of X

(m + X) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(y,(y \ x)) to_power ((m + X) + 1) is Element of the carrier of X

(((y,(y \ x)) to_power ((m + X) + 1)),(x \ y)) to_power n is Element of the carrier of X

(X,y,x,m,n) is Element of the carrier of X

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(y,(y \ x)) to_power (m + 1) is Element of the carrier of X

(((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power n is Element of the carrier of X

((X,y,x,m,n),(y \ x)) to_power X is Element of the carrier of X

(((y,(y \ x)) to_power (m + 1)),(y \ x)) to_power X is Element of the carrier of X

(((((y,(y \ x)) to_power (m + 1)),(y \ x)) to_power X),(x \ y)) to_power n is Element of the carrier of X

(m + 1) + X is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(y,(y \ x)) to_power ((m + 1) + X) is Element of the carrier of X

(((y,(y \ x)) to_power ((m + 1) + X)),(x \ y)) to_power n is Element of the carrier of X

(X,x,y,i,j) is Element of the carrier of X

(((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power j is Element of the carrier of X

((X,x,y,i,j),(y \ x)) to_power X is Element of the carrier of X

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)

the carrier of X is non empty set

X is Element of the carrier of X

x is Element of the carrier of X

(X,x) to_power (i + 1) is Element of the carrier of X

(X,x) to_power (n + 1) is Element of the carrier of X

X \ x is Element of the carrier of X

(X \ x) \ X is Element of the carrier of X

X \ X is Element of the carrier of X

(X \ X) \ x is Element of the carrier of X

x ` is Element of the carrier of X

0. X is V49(X) minimal positive V92(X) Element of the carrier of X

(0. X) \ x is Element of the carrier of X

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,(X \ x),X,(m + 1),n) is Element of the carrier of X

(m + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

((X \ x),((X \ x) \ X)) to_power ((m + 1) + 1) is Element of the carrier of X

X \ (X \ x) is Element of the carrier of X

((((X \ x),((X \ x) \ X)) to_power ((m + 1) + 1)),(X \ (X \ x))) to_power n is Element of the carrier of X

((X \ x),(X \ (X \ x))) to_power n is Element of the carrier of X

X \ (X \ (X \ x)) is Element of the carrier of X

((X \ (X \ (X \ x))),(X \ (X \ x))) to_power n is Element of the carrier of X

(X,(X \ (X \ x))) to_power 1 is Element of the carrier of X

(((X,(X \ (X \ x))) to_power 1),(X \ (X \ x))) to_power n is Element of the carrier of X

(X,(X \ (X \ x))) to_power (n + 1) is Element of the carrier of X

j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,X,(X \ x),i,(j + 1)) is Element of the carrier of X

(X,(X \ (X \ x))) to_power (i + 1) is Element of the carrier of X

(((X,(X \ (X \ x))) to_power (i + 1)),((X \ x) \ X)) to_power (j + 1) is Element of the carrier of X

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)

the carrier of X is non empty set

X is Element of the carrier of X

x is Element of the carrier of X

(X,x) to_power (j + 1) is Element of the carrier of X

(X,x) to_power (m + 1) is Element of the carrier of X

X \ x is Element of the carrier of X

(X \ x) \ X is Element of the carrier of X

X \ X is Element of the carrier of X

(X \ X) \ x is Element of the carrier of X

x ` is Element of the carrier of X

0. X is V49(X) minimal positive V92(X) Element of the carrier of X

(0. X) \ x is Element of the carrier of X

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,(X \ x),X,(i + 1),j) is Element of the carrier of X

(i + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

((X \ x),((X \ x) \ X)) to_power ((i + 1) + 1) is Element of the carrier of X

X \ (X \ x) is Element of the carrier of X

((((X \ x),((X \ x) \ X)) to_power ((i + 1) + 1)),(X \ (X \ x))) to_power j is Element of the carrier of X

((X \ x),(X \ (X \ x))) to_power j is Element of the carrier of X

X \ (X \ (X \ x)) is Element of the carrier of X

((X \ (X \ (X \ x))),(X \ (X \ x))) to_power j is Element of the carrier of X

(X,(X \ (X \ x))) to_power 1 is Element of the carrier of X

(((X,(X \ (X \ x))) to_power 1),(X \ (X \ x))) to_power j is Element of the carrier of X

(X,(X \ (X \ x))) to_power (j + 1) is Element of the carrier of X

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,X,(X \ x),m,(n + 1)) is Element of the carrier of X

(X,(X \ (X \ x))) to_power (m + 1) is Element of the carrier of X

(((X,(X \ (X \ x))) to_power (m + 1)),((X \ x) \ X)) to_power (n + 1) is Element of the carrier of X

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)

the carrier of X is non empty set

X is Element of the carrier of X

x is Element of the carrier of X

(X,X,x,i,j) is Element of the carrier of X

X \ x is Element of the carrier of X

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,(X \ x)) to_power (i + 1) is Element of the carrier of X

x \ X is Element of the carrier of X

(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power j is Element of the carrier of X

(X,x,X,j,n) is Element of the carrier of X

j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ X)) to_power (j + 1) is Element of the carrier of X

(((x,(x \ X)) to_power (j + 1)),(X \ x)) to_power n is Element of the carrier of X

(X,x,X,m,n) is Element of the carrier of X

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ X)) to_power (m + 1) is Element of the carrier of X

(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power n is Element of the carrier of X

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)

the carrier of X is non empty set

X is Element of the carrier of X

x is Element of the carrier of X

(X,X,x,n,j) is Element of the carrier of X

X \ x is Element of the carrier of X

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,(X \ x)) to_power (n + 1) is Element of the carrier of X

x \ X is Element of the carrier of X

(((X,(X \ x)) to_power (n + 1)),(x \ X)) to_power j is Element of the carrier of X

(X,x,X,m,n) is Element of the carrier of X

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ X)) to_power (m + 1) is Element of the carrier of X

(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power n is Element of the carrier of X

(X,X,x,i,j) is Element of the carrier of X

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,(X \ x)) to_power (i + 1) is Element of the carrier of X

(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power j is Element of the carrier of X

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

min (i,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

min (m,n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

min ((min (i,j)),(min (m,n))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

max (i,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

max (m,n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

max ((max (i,j)),(max (m,n))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

(i,j,m,n) is ext-real set

min (i,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

min (m,n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

min ((min (i,j)),(min (m,n))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

(i,j,m,n) is ext-real set

max (i,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

max (m,n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

max ((max (i,j)),(max (m,n))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

(i,j,m,n) is ext-real set

min (i,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

min (m,n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

min ((min (i,j)),(min (m,n))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

(i,j,m,n) is ext-real set

max (i,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

max (m,n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

max ((max (i,j)),(max (m,n))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

(i,j,m,n) is ext-real set

min (i,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

min (m,n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

min ((min (i,j)),(min (m,n))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)

the carrier of X is non empty set

X is Element of the carrier of X

x is Element of the carrier of X

(X,X,x,i,i) is Element of the carrier of X

X \ x is Element of the carrier of X

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,(X \ x)) to_power (i + 1) is Element of the carrier of X

x \ X is Element of the carrier of X

(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power i is Element of the carrier of X

(X,x,X,i,i) is Element of the carrier of X

(x,(x \ X)) to_power (i + 1) is Element of the carrier of X

(((x,(x \ X)) to_power (i + 1)),(X \ x)) to_power i is Element of the carrier of X

(((x,(x \ X)) to_power (i + 1)),(X \ x)) to_power n is Element of the carrier of X

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ X)) to_power (m + 1) is Element of the carrier of X

(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power n is Element of the carrier of X

(X,X,x,i,j) is Element of the carrier of X

(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power j is Element of the carrier of X

(X,x,X,m,n) is Element of the carrier of X

x is Element of the carrier of X

X is Element of the carrier of X

(X,x,X,i,i) is Element of the carrier of X

x \ X is Element of the carrier of X

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ X)) to_power (i + 1) is Element of the carrier of X

X \ x is Element of the carrier of X

(((x,(x \ X)) to_power (i + 1)),(X \ x)) to_power i is Element of the carrier of X

(X,X,x,i,i) is Element of the carrier of X

(X,(X \ x)) to_power (i + 1) is Element of the carrier of X

(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power i is Element of the carrier of X

(X,X,x,i,i) \ (X,x,X,i,i) is Element of the carrier of X

0. X is V49(X) minimal positive V92(X) Element of the carrier of X

(X,x,X,i,i) \ (X,X,x,i,i) is Element of the carrier of X

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

(i,j,m,n) is ext-real set

min (i,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

min (m,n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

min ((min (i,j)),(min (m,n))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)

the carrier of X is non empty set

n - i is V11() V12() ext-real Element of REAL

i - i is V11() V12() ext-real Element of REAL

1 + i is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(n - i) + i is V11() V12() ext-real Element of REAL

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

j - i is V11() V12() ext-real Element of REAL

(j - i) + i is V11() V12() ext-real Element of REAL

X is Element of the carrier of X

x is Element of the carrier of X

(X,X,x,i,(i + 1)) is Element of the carrier of X

X \ x is Element of the carrier of X

(X,(X \ x)) to_power (i + 1) is Element of the carrier of X

x \ X is Element of the carrier of X

(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power (i + 1) is Element of the carrier of X

(X,x,X,i,(i + 1)) is Element of the carrier of X

(x,(x \ X)) to_power (i + 1) is Element of the carrier of X

(((x,(x \ X)) to_power (i + 1)),(X \ x)) to_power (i + 1) is Element of the carrier of X

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ X)) to_power (n + 1) is Element of the carrier of X

(x,(x \ X)) to_power (m + 1) is Element of the carrier of X

(X,X,x,i,j) is Element of the carrier of X

(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power j is Element of the carrier of X

(X,x,X,m,n) is Element of the carrier of X

(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power n is Element of the carrier of X

(((x,(x \ X)) to_power (i + 1)),(X \ x)) to_power (n + 1) is Element of the carrier of X

(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power (n + 1) is Element of the carrier of X

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

(i,j,m,n) is ext-real set

min (i,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

min (m,n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

min ((min (i,j)),(min (m,n))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)

the carrier of X is non empty set

X is Element of the carrier of X

x is Element of the carrier of X

(X,X,x,i,i) is Element of the carrier of X

X \ x is Element of the carrier of X

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,(X \ x)) to_power (i + 1) is Element of the carrier of X

x \ X is Element of the carrier of X

(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power i is Element of the carrier of X

(X,x,X,i,j) is Element of the carrier of X

(x,(x \ X)) to_power (i + 1) is Element of the carrier of X

(((x,(x \ X)) to_power (i + 1)),(X \ x)) to_power j is Element of the carrier of X

(i,i,i,j) is ext-real set

min (i,i) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

min ((min (i,i)),(min (i,j))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)

the carrier of X is non empty set

j - m is V11() V12() ext-real Element of REAL

m - m is V11() V12() ext-real Element of REAL

1 + m is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(j - m) + m is V11() V12() ext-real Element of REAL

X is Element of the carrier of X

x is Element of the carrier of X

(X,X,x,i,(m + 1)) is Element of the carrier of X

X \ x is Element of the carrier of X

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,(X \ x)) to_power (i + 1) is Element of the carrier of X

x \ X is Element of the carrier of X

(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power (m + 1) is Element of the carrier of X

(X,x,X,m,i) is Element of the carrier of X

(x,(x \ X)) to_power (m + 1) is Element of the carrier of X

(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power i is Element of the carrier of X

j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,X,x,i,j) is Element of the carrier of X

(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power j is Element of the carrier of X

(X,x,X,m,n) is Element of the carrier of X

(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power n is Element of the carrier of X

(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power (j + 1) is Element of the carrier of X

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,i)

the carrier of X is non empty set

x is Element of the carrier of X

y is Element of the carrier of X

(X,x,y,i,j) is Element of the carrier of X

x \ y is Element of the carrier of X

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ y)) to_power (i + 1) is Element of the carrier of X

y \ x is Element of the carrier of X

(((x,(x \ y)) to_power (i + 1)),(y \ x)) to_power j is Element of the carrier of X

(X,y,x,j,i) is Element of the carrier of X

j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(y,(y \ x)) to_power (j + 1) is Element of the carrier of X

(((y,(y \ x)) to_power (j + 1)),(x \ y)) to_power i is Element of the carrier of X

(X,y,x,m,i) is Element of the carrier of X

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(y,(y \ x)) to_power (m + 1) is Element of the carrier of X

(((y,(y \ x)) to_power (m + 1)),(x \ y)) to_power i is Element of the carrier of X

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

x is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)

X - j is V11() V12() ext-real Element of REAL

y is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X - n is V11() V12() ext-real Element of REAL

t1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n + t1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j + y is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

(i,j,m,n) is ext-real set

max (i,j) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

max (m,n) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

max ((max (i,j)),(max (m,n))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)

X - n is V11() V12() ext-real Element of REAL

x is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X - j is V11() V12() ext-real Element of REAL

y is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n + x is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j + y is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)

the carrier of X is non empty set

X is Element of the carrier of X

x is Element of the carrier of X

(X,X,x,i,j) is Element of the carrier of X

X \ x is Element of the carrier of X

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,(X \ x)) to_power (i + 1) is Element of the carrier of X

x \ X is Element of the carrier of X

(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power j is Element of the carrier of X

(X,x,X,i,j) is Element of the carrier of X

(x,(x \ X)) to_power (i + 1) is Element of the carrier of X

(((x,(x \ X)) to_power (i + 1)),(X \ x)) to_power j is Element of the carrier of X

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ X)) to_power (m + 1) is Element of the carrier of X

(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power n is Element of the carrier of X

(((x,(x \ X)) to_power (i + 1)),(X \ x)) to_power n is Element of the carrier of X

(X,x,X,m,n) is Element of the carrier of X

x is Element of the carrier of X

X is Element of the carrier of X

(X,x,X,i,j) is Element of the carrier of X

x \ X is Element of the carrier of X

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ X)) to_power (i + 1) is Element of the carrier of X

X \ x is Element of the carrier of X

(((x,(x \ X)) to_power (i + 1)),(X \ x)) to_power j is Element of the carrier of X

(X,X,x,i,j) is Element of the carrier of X

(X,(X \ x)) to_power (i + 1) is Element of the carrier of X

(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power j is Element of the carrier of X

(X,X,x,i,j) \ (X,x,X,i,j) is Element of the carrier of X

0. X is V49(X) minimal positive V92(X) Element of the carrier of X

(X,x,X,i,j) \ (X,X,x,i,j) is Element of the carrier of X

i is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

X is non empty being_B being_C being_I being_BCI-4 being_BCK-5 (i,j,m,n)

the carrier of X is non empty set

n - i is V11() V12() ext-real Element of REAL

i - i is V11() V12() ext-real Element of REAL

1 + i is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(n - i) + i is V11() V12() ext-real Element of REAL

X is Element of the carrier of X

x is Element of the carrier of X

(X,X,x,i,j) is Element of the carrier of X

X \ x is Element of the carrier of X

(X,(X \ x)) to_power (i + 1) is Element of the carrier of X

x \ X is Element of the carrier of X

(((X,(X \ x)) to_power (i + 1)),(x \ X)) to_power j is Element of the carrier of X

(X,x,X,i,(i + 1)) is Element of the carrier of X

(x,(x \ X)) to_power (i + 1) is Element of the carrier of X

(((x,(x \ X)) to_power (i + 1)),(X \ x)) to_power (i + 1) is Element of the carrier of X

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,x,X,m,n) is Element of the carrier of X

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(x,(x \ X)) to_power (m + 1) is Element of the carrier of X

(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power n is Element of the carrier of X

(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power (i + 1) is Element of the carrier of X

(((x,(x \ X)) to_power (m + 1)),(X \ x)) to_power (n + 1) is Element of the carrier of X

(x,(x \ X)) to_power (n + 1) is Element of the carrier of X

i is non empty being_B being_C being_I being_BCI-4 BCIStr_0

j is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

m + n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

j + n is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative Element of NAT

the carrier of i is non empty set

0. i is V49(i) minimal positive V92(i) Element of the carrier of i

X is Element of the carrier of i

(0. i) \ X is Element of the carrier of i

(m + n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

(X,X) to_power ((m + n) + 1) is Element of the carrier of i

(((X,X) to_power ((m + n) + 1)),((0. i) \ X)) to_power (j + n) is Element of the carrier of i

(X,X) to_power (m + n) is Element of the carrier of i

((X,X) to_power (m + n)) \ X is Element of the carrier of i

((((X,X) to_power (m + n)) \ X),((0. i) \ X)) to_power (j + n) is Element of the carrier of i

X \ X is Element of the carrier of i

((X \ X),X) to_power (m + n) is Element of the carrier of i

((((X \ X),X) to_power (m + n)),((0. i) \ X)) to_power (j + n) is Element of the carrier of i

((0. i),X) to_power (m + n) is Element of the carrier of i

((((0. i),X) to_power (m + n)),((0. i) \ X)) to_power (j + n) is Element of the carrier of i

((0. i),((0. i) \ X)) to_power (j + n) is Element of the carrier of i

((((0. i),((0. i) \ X)) to_power (j + n)),X) to_power (m + n) is Element of the carrier of i

((0. i),(0. i)) to_power (j + n) is Element of the carrier of i

((0. i),X) to_power (j + n) is Element of the carrier of i

(((0. i),(0. i)) to_power (j + n)) \ (((0. i),X) to_power (j + n)) is Element of the carrier of i

(((((0. i),(0. i)) to_power (j + n)) \ (((0. i),X) to_power (j + n))),X) to_power (m + n) is Element of the carrier of i

(0. i) \ (((0. i),X) to_power (j + n)) is Element of the carrier of i

(((0. i) \ (((0. i),X) to_power (j + n))),X) to_power (m + n) is Element of the carrier of i

(((0. i),X) to_power (m + n)) \ (((0. i),X) to_power (j + n)) is Element of the carrier of i

((0. i),X) to_power m is Element of the carrier of i

((((0. i),X) to_power m),X) to_power n is Element of the carrier of i

(((((0. i),X) to_power m),X) to_power n) \ (((0. i),X) to_power (j + n)) is Element of the carrier of i

((0. i),X) to_power j is Element of the carrier of i

((((0. i),X) to_power j),X) to_power n is Element of the carrier of i

(((((0. i),X) to_power m),X) to_power n) \ (((((0. i),X) to_power j),X) to_power n) is Element of the carrier of i

(((0. i),X) to_power m) \ (((0. i),X) to_power j) is Element of the carrier of i

(i,(0. i),X,j,m) is Element of the carrier of i

j + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative Element of NAT

((0. i),((0. i) \ X)) to_power (j + 1) is Element of the carrier of i

X \ (0. i) is Element of the carrier of i

((((0. i),((0. i) \ X)) to_power (j + 1)),(X \ (0. i))) to_power m is Element of the carrier of i

(i,X,(0. i),(m + n),(j + n)) is