:: BCIALG_4 semantic presentation

REAL is set

NAT is non empty V24() V25() V26() V33() V38() V39() Element of bool REAL

bool REAL is set

NAT is non empty V24() V25() V26() V33() V38() V39() set

bool NAT is V33() set

bool NAT is V33() set

K186(NAT) is V131() set

{} is set

1 is non empty V24() V25() V26() V30() V33() V38() ext-real Element of NAT

[:1,1:] is Relation-like set

bool [:1,1:] is set

[:[:1,1:],1:] is Relation-like set

bool [:[:1,1:],1:] is set

Seg 1 is Element of bool NAT

{ b

0 is V24() V25() V26() V30() V33() V38() ext-real Element of NAT

{{}} is non empty trivial V40(1) set

the non empty set is non empty set

[: the non empty set , the non empty set :] is Relation-like set

[:[: the non empty set , the non empty set :], the non empty set :] is Relation-like set

bool [:[: the non empty set , the non empty set :], the non empty set :] is set

the Relation-like Function-like V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :] is Relation-like Function-like V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :]

the Element of the non empty set is Element of the non empty set

( the non empty set , the Relation-like Function-like V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Relation-like Function-like V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Element of the non empty set ) is () ()

the carrier of ( the non empty set , the Relation-like Function-like V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Relation-like Function-like V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Element of the non empty set ) is set

X is ()

the carrier of X is set

the of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is Relation-like set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

x is Element of the carrier of X

y is Element of the carrier of X

the of X . (x,y) is Element of the carrier of X

[x,y] is set

the of X . [x,y] is set

op2 is Relation-like Function-like V18([:1,1:],1) Element of bool [:[:1,1:],1:]

op0 is V24() V25() V26() Element of 1

(1,op2,op2,op0) is () ()

() is ()

the carrier of () is non empty trivial V33() V40(1) set

X is Element of the carrier of ()

x is Element of the carrier of ()

X \ x is Element of the carrier of ()

the InternalDiff of () is Relation-like Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]

[: the carrier of (), the carrier of ():] is Relation-like set

[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like set

bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set

the InternalDiff of () . (X,x) is Element of the carrier of ()

[X,x] is set

the InternalDiff of () . [X,x] is set

y is Element of the carrier of ()

y \ x is Element of the carrier of ()

the InternalDiff of () . (y,x) is Element of the carrier of ()

[y,x] is set

the InternalDiff of () . [y,x] is set

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

the InternalDiff of () . ((X \ x),(y \ x)) is Element of the carrier of ()

[(X \ x),(y \ x)] is set

the InternalDiff of () . [(X \ x),(y \ x)] is set

X \ y is Element of the carrier of ()

the InternalDiff of () . (X,y) is Element of the carrier of ()

[X,y] is set

the InternalDiff of () . [X,y] is set

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

the InternalDiff of () . (((X \ x) \ (y \ x)),(X \ y)) is Element of the carrier of ()

[((X \ x) \ (y \ x)),(X \ y)] is set

the InternalDiff of () . [((X \ x) \ (y \ x)),(X \ y)] is set

0. () is V49(()) Element of the carrier of ()

the ZeroF of () is Element of the carrier of ()

the carrier of () is non empty trivial V33() V40(1) set

X is Element of the carrier of ()

x is Element of the carrier of ()

X \ x is Element of the carrier of ()

the InternalDiff of () is Relation-like Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]

[: the carrier of (), the carrier of ():] is Relation-like set

[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like set

bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set

the InternalDiff of () . (X,x) is Element of the carrier of ()

[X,x] is set

the InternalDiff of () . [X,x] is set

y is Element of the carrier of ()

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

the InternalDiff of () . ((X \ x),y) is Element of the carrier of ()

[(X \ x),y] is set

the InternalDiff of () . [(X \ x),y] is set

X \ y is Element of the carrier of ()

the InternalDiff of () . (X,y) is Element of the carrier of ()

[X,y] is set

the InternalDiff of () . [X,y] is set

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

the InternalDiff of () . ((X \ y),x) is Element of the carrier of ()

[(X \ y),x] is set

the InternalDiff of () . [(X \ y),x] is set

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

the InternalDiff of () . (((X \ x) \ y),((X \ y) \ x)) is Element of the carrier of ()

[((X \ x) \ y),((X \ y) \ x)] is set

the InternalDiff of () . [((X \ x) \ y),((X \ y) \ x)] is set

0. () is V49(()) Element of the carrier of ()

the ZeroF of () is Element of the carrier of ()

the carrier of () is non empty trivial V33() V40(1) set

X is Element of the carrier of ()

X \ X is Element of the carrier of ()

the InternalDiff of () is Relation-like Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]

[: the carrier of (), the carrier of ():] is Relation-like set

[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like set

bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set

the InternalDiff of () . (X,X) is Element of the carrier of ()

[X,X] is set

the InternalDiff of () . [X,X] is set

0. () is V49(()) Element of the carrier of ()

the ZeroF of () is Element of the carrier of ()

the carrier of () is non empty trivial V33() V40(1) set

X is Element of the carrier of ()

x is Element of the carrier of ()

X \ x is Element of the carrier of ()

the InternalDiff of () is Relation-like Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]

[: the carrier of (), the carrier of ():] is Relation-like set

[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like set

bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set

the InternalDiff of () . (X,x) is Element of the carrier of ()

[X,x] is set

the InternalDiff of () . [X,x] is set

0. () is V49(()) Element of the carrier of ()

the ZeroF of () is Element of the carrier of ()

x \ X is Element of the carrier of ()

the InternalDiff of () . (x,X) is Element of the carrier of ()

[x,X] is set

the InternalDiff of () . [x,X] is set

the carrier of () is non empty trivial V33() V40(1) set

X is Element of the carrier of ()

X ` is Element of the carrier of ()

0. () is V49(()) Element of the carrier of ()

the ZeroF of () is Element of the carrier of ()

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

the InternalDiff of () is Relation-like Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]

[: the carrier of (), the carrier of ():] is Relation-like set

[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like set

bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set

the InternalDiff of () . ((0. ()),X) is Element of the carrier of ()

[(0. ()),X] is set

the InternalDiff of () . [(0. ()),X] is set

the carrier of () is non empty trivial V33() V40(1) set

X is Element of the carrier of ()

x is Element of the carrier of ()

X \ x is Element of the carrier of ()

the InternalDiff of () is Relation-like Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]

[: the carrier of (), the carrier of ():] is Relation-like set

[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like set

bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set

the InternalDiff of () . (X,x) is Element of the carrier of ()

[X,x] is set

the InternalDiff of () . [X,x] is set

y is Element of the carrier of ()

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

the InternalDiff of () . ((X \ x),y) is Element of the carrier of ()

[(X \ x),y] is set

the InternalDiff of () . [(X \ x),y] is set

((),x,y) is Element of the carrier of ()

the of () is Relation-like Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]

the of () . (x,y) is Element of the carrier of ()

[x,y] is set

the of () . [x,y] is set

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

the InternalDiff of () . (X,((),x,y)) is Element of the carrier of ()

[X,((),x,y)] is set

the InternalDiff of () . [X,((),x,y)] is set

X is non empty being_B being_C being_I being_BCI-4 () ()

the carrier of X is non empty set

x is Element of the carrier of X

y is Element of the carrier of X

{ b

bool the carrier of X is set

0. X is V49(X) V142(X) positive nilpotent Element of the carrier of X

the ZeroF of X is Element of the carrier of X

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

the InternalDiff of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is Relation-like set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . ((0. X),x) is Element of the carrier of X

[(0. X),x] is set

the InternalDiff of X . [(0. X),x] is set

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

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

[((0. X) \ x),y] is set

the InternalDiff of X . [((0. X) \ x),y] is set

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

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

[(0. X),(((0. X) \ x) \ y)] is set

the InternalDiff of X . [(0. X),(((0. X) \ x) \ y)] is set

x is set

x2 is Element of the carrier of X

x2 \ x is Element of the carrier of X

the InternalDiff of X . (x2,x) is Element of the carrier of X

[x2,x] is set

the InternalDiff of X . [x2,x] is set

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

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

[((0. X) \ (((0. X) \ x) \ y)),x] is set

the InternalDiff of X . [((0. X) \ (((0. X) \ x) \ y)),x] is set

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

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

[(((0. X) \ (((0. X) \ x) \ y)) \ x),y] is set

the InternalDiff of X . [(((0. X) \ (((0. X) \ x) \ y)) \ x),y] is set

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

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

[((0. X) \ x),(((0. X) \ x) \ y)] is set

the InternalDiff of X . [((0. X) \ x),(((0. X) \ x) \ y)] is set

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

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

[(((0. X) \ x) \ (((0. X) \ x) \ y)),y] is set

the InternalDiff of X . [(((0. X) \ x) \ (((0. X) \ x) \ y)),y] is set

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

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

[((0. X) \ x),(0. X)] is set

the InternalDiff of X . [((0. X) \ x),(0. X)] is set

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

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

[(((0. X) \ x) \ (0. X)),(((0. X) \ x) \ y)] is set

the InternalDiff of X . [(((0. X) \ x) \ (0. X)),(((0. X) \ x) \ y)] is set

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

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

[((((0. X) \ x) \ (0. X)) \ (((0. X) \ x) \ y)),y] is set

the InternalDiff of X . [((((0. X) \ x) \ (0. X)) \ (((0. X) \ x) \ y)),y] is set

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

the InternalDiff of X . (y,(0. X)) is Element of the carrier of X

[y,(0. X)] is set

the InternalDiff of X . [y,(0. X)] is set

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

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

[((((0. X) \ x) \ (0. X)) \ (((0. X) \ x) \ y)),(y \ (0. X))] is set

the InternalDiff of X . [((((0. X) \ x) \ (0. X)) \ (((0. X) \ x) \ y)),(y \ (0. X))] is set

X is non empty being_B being_C being_I being_BCI-4 () ()

the carrier of X is non empty set

z is Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

(X,x,y) is non empty Element of bool the carrier of X

bool the carrier of X is set

{ b

u is Element of the carrier of X

u \ x is Element of the carrier of X

the InternalDiff of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is Relation-like set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . (u,x) is Element of the carrier of X

[u,x] is set

the InternalDiff of X . [u,x] is set

z \ x is Element of the carrier of X

the InternalDiff of X . (z,x) is Element of the carrier of X

[z,x] is set

the InternalDiff of X . [z,x] is set

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

the InternalDiff of X . ((u \ x),(z \ x)) is Element of the carrier of X

[(u \ x),(z \ x)] is set

the InternalDiff of X . [(u \ x),(z \ x)] is set

0. X is V49(X) V142(X) positive nilpotent Element of the carrier of X

the ZeroF of X is Element of the carrier of X

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

the InternalDiff of X . ((z \ x),y) is Element of the carrier of X

[(z \ x),y] is set

the InternalDiff of X . [(z \ x),y] is set

x is Element of the carrier of X

x \ x is Element of the carrier of X

the InternalDiff of X . (x,x) is Element of the carrier of X

[x,x] is set

the InternalDiff of X . [x,x] is set

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

the InternalDiff of X . ((u \ x),y) is Element of the carrier of X

[(u \ x),y] is set

the InternalDiff of X . [(u \ x),y] is set

X is non empty being_B being_C being_I being_BCI-4 () ()

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) is non empty Element of bool the carrier of X

bool the carrier of X is set

{ b

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

the of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is Relation-like set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the of X . (x,y) is Element of the carrier of X

[x,y] is set

the of X . [x,y] is set

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

the InternalDiff of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

the InternalDiff of X . ((X,x,y),x) is Element of the carrier of X

[(X,x,y),x] is set

the InternalDiff of X . [(X,x,y),x] is set

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

the InternalDiff of X . (((X,x,y) \ x),y) is Element of the carrier of X

[((X,x,y) \ x),y] is set

the InternalDiff of X . [((X,x,y) \ x),y] is set

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

the InternalDiff of X . ((X,x,y),(X,x,y)) is Element of the carrier of X

[(X,x,y),(X,x,y)] is set

the InternalDiff of X . [(X,x,y),(X,x,y)] is set

0. X is V49(X) V142(X) positive nilpotent Element of the carrier of X

the ZeroF of X is Element of the carrier of X

z is Element of (X,x,y)

u is Element of (X,x,y)

x is Element of the carrier of X

x \ x is Element of the carrier of X

the InternalDiff of X . (x,x) is Element of the carrier of X

[x,x] is set

the InternalDiff of X . [x,x] is set

u \ z is Element of the carrier of X

the InternalDiff of X . (u,z) is Element of the carrier of X

[u,z] is set

the InternalDiff of X . [u,z] is set

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

the InternalDiff of X . ((x \ x),y) is Element of the carrier of X

[(x \ x),y] is set

the InternalDiff of X . [(x \ x),y] is set

u is Element of (X,x,y)

X is non empty being_B being_C being_I being_BCI-4 () ()

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) is Element of the carrier of X

the of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is Relation-like set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the of X . (x,y) is Element of the carrier of X

[x,y] is set

the of X . [x,y] is set

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

the InternalDiff of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

the InternalDiff of X . ((X,x,y),x) is Element of the carrier of X

[(X,x,y),x] is set

the InternalDiff of X . [(X,x,y),x] is set

z is Element of the carrier of X

z \ x is Element of the carrier of X

the InternalDiff of X . (z,x) is Element of the carrier of X

[z,x] is set

the InternalDiff of X . [z,x] is set

z \ (X,x,y) is Element of the carrier of X

the InternalDiff of X . (z,(X,x,y)) is Element of the carrier of X

[z,(X,x,y)] is set

the InternalDiff of X . [z,(X,x,y)] is set

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

the InternalDiff of X . ((z \ x),y) is Element of the carrier of X

[(z \ x),y] is set

the InternalDiff of X . [(z \ x),y] is set

0. X is V49(X) V142(X) positive nilpotent Element of the carrier of X

the ZeroF of X is Element of the carrier of X

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

the InternalDiff of X . (((X,x,y) \ x),y) is Element of the carrier of X

[((X,x,y) \ x),y] is set

the InternalDiff of X . [((X,x,y) \ x),y] is set

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

the InternalDiff of X . ((X,x,y),(X,x,y)) is Element of the carrier of X

[(X,x,y),(X,x,y)] is set

the InternalDiff of X . [(X,x,y),(X,x,y)] is set

0. X is V49(X) V142(X) positive nilpotent Element of the carrier of X

the ZeroF of X is Element of the carrier of X

z is Element of the carrier of X

z \ x is Element of the carrier of X

the InternalDiff of X . (z,x) is Element of the carrier of X

[z,x] is set

the InternalDiff of X . [z,x] is set

X is non empty ()

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 \ y is Element of the carrier of X

the InternalDiff of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is Relation-like set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . (x,y) is Element of the carrier of X

[x,y] is set

the InternalDiff of X . [x,y] is set

z is Element of the carrier of X

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

the InternalDiff of X . ((x \ y),z) is Element of the carrier of X

[(x \ y),z] is set

the InternalDiff of X . [(x \ y),z] is set

(X,y,z) is Element of the carrier of X

the of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

the of X . (y,z) is Element of the carrier of X

[y,z] is set

the of X . [y,z] is set

x \ (X,y,z) is Element of the carrier of X

the InternalDiff of X . (x,(X,y,z)) is Element of the carrier of X

[x,(X,y,z)] is set

the InternalDiff of X . [x,(X,y,z)] is set

(X,y,z) \ y is Element of the carrier of X

the InternalDiff of X . ((X,y,z),y) is Element of the carrier of X

[(X,y,z),y] is set

the InternalDiff of X . [(X,y,z),y] is set

((X,y,z) \ y) \ z is Element of the carrier of X

the InternalDiff of X . (((X,y,z) \ y),z) is Element of the carrier of X

[((X,y,z) \ y),z] is set

the InternalDiff of X . [((X,y,z) \ y),z] is set

0. X is V49(X) Element of the carrier of X

the ZeroF of X is Element of the carrier of X

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

the InternalDiff of X . (x,((x \ y) \ z)) is Element of the carrier of X

[x,((x \ y) \ z)] is set

the InternalDiff of X . [x,((x \ y) \ z)] is set

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

the InternalDiff of X . ((x \ ((x \ y) \ z)),y) is Element of the carrier of X

[(x \ ((x \ y) \ z)),y] is set

the InternalDiff of X . [(x \ ((x \ y) \ z)),y] is set

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

the InternalDiff of X . ((x \ y),((x \ y) \ z)) is Element of the carrier of X

[(x \ y),((x \ y) \ z)] is set

the InternalDiff of X . [(x \ y),((x \ y) \ z)] is set

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

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

[(x \ y),(0. X)] is set

the InternalDiff of X . [(x \ y),(0. X)] is set

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

the InternalDiff of X . (((x \ y) \ (0. X)),((x \ y) \ z)) is Element of the carrier of X

[((x \ y) \ (0. X)),((x \ y) \ z)] is set

the InternalDiff of X . [((x \ y) \ (0. X)),((x \ y) \ z)] is set

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

the InternalDiff of X . (z,(0. X)) is Element of the carrier of X

[z,(0. X)] is set

the InternalDiff of X . [z,(0. X)] is set

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

the InternalDiff of X . (((x \ ((x \ y) \ z)) \ y),(z \ (0. X))) is Element of the carrier of X

[((x \ ((x \ y) \ z)) \ y),(z \ (0. X))] is set

the InternalDiff of X . [((x \ ((x \ y) \ z)) \ y),(z \ (0. X))] is set

(x \ ((x \ y) \ z)) \ (X,y,z) is Element of the carrier of X

the InternalDiff of X . ((x \ ((x \ y) \ z)),(X,y,z)) is Element of the carrier of X

[(x \ ((x \ y) \ z)),(X,y,z)] is set

the InternalDiff of X . [(x \ ((x \ y) \ z)),(X,y,z)] is set

(x \ (X,y,z)) \ ((x \ y) \ z) is Element of the carrier of X

the InternalDiff of X . ((x \ (X,y,z)),((x \ y) \ z)) is Element of the carrier of X

[(x \ (X,y,z)),((x \ y) \ z)] is set

the InternalDiff of X . [(x \ (X,y,z)),((x \ y) \ z)] is set

(x \ y) \ (x \ (X,y,z)) is Element of the carrier of X

the InternalDiff of X . ((x \ y),(x \ (X,y,z))) is Element of the carrier of X

[(x \ y),(x \ (X,y,z))] is set

the InternalDiff of X . [(x \ y),(x \ (X,y,z))] is set

((x \ y) \ (x \ (X,y,z))) \ ((X,y,z) \ y) is Element of the carrier of X

the InternalDiff of X . (((x \ y) \ (x \ (X,y,z))),((X,y,z) \ y)) is Element of the carrier of X

[((x \ y) \ (x \ (X,y,z))),((X,y,z) \ y)] is set

the InternalDiff of X . [((x \ y) \ (x \ (X,y,z))),((X,y,z) \ y)] is set

((x \ y) \ (x \ (X,y,z))) \ z is Element of the carrier of X

the InternalDiff of X . (((x \ y) \ (x \ (X,y,z))),z) is Element of the carrier of X

[((x \ y) \ (x \ (X,y,z))),z] is set

the InternalDiff of X . [((x \ y) \ (x \ (X,y,z))),z] is set

((x \ y) \ z) \ (x \ (X,y,z)) is Element of the carrier of X

the InternalDiff of X . (((x \ y) \ z),(x \ (X,y,z))) is Element of the carrier of X

[((x \ y) \ z),(x \ (X,y,z))] is set

the InternalDiff of X . [((x \ y) \ z),(x \ (X,y,z))] is set

x is non empty ()

the carrier of x is non empty set

X is non empty ()

the carrier of X is non empty set

y is Element of the carrier of x

z is Element of the carrier of x

(x,y,z) is Element of the carrier of x

the of x is Relation-like Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]

[: the carrier of x, the carrier of x:] is Relation-like set

[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like set

bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set

the of x . (y,z) is Element of the carrier of x

[y,z] is set

the of x . [y,z] is set

(x,y,z) \ y is Element of the carrier of x

the InternalDiff of x is Relation-like Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]

the InternalDiff of x . ((x,y,z),y) is Element of the carrier of x

[(x,y,z),y] is set

the InternalDiff of x . [(x,y,z),y] is set

x2 is Element of the carrier of x

u is Element of the carrier of x

x2 \ u is Element of the carrier of x

the InternalDiff of x . (x2,u) is Element of the carrier of x

[x2,u] is set

the InternalDiff of x . [x2,u] is set

x is Element of the carrier of x

(x,u,x) is Element of the carrier of x

the of x . (u,x) is Element of the carrier of x

[u,x] is set

the of x . [u,x] is set

X is non empty being_B being_C being_I being_BCI-4 () ()

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) is non empty Element of bool the carrier of X

bool the carrier of X is set

{ b

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

the of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is Relation-like set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the of X . (x,y) is Element of the carrier of X

[x,y] is set

the of X . [x,y] is set

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

the InternalDiff of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

the InternalDiff of X . ((X,x,y),x) is Element of the carrier of X

[(X,x,y),x] is set

the InternalDiff of X . [(X,x,y),x] is set

z is Element of (X,x,y)

u is Element of (X,x,y)

x is Element of the carrier of X

x \ x is Element of the carrier of X

the InternalDiff of X . (x,x) is Element of the carrier of X

[x,x] is set

the InternalDiff of X . [x,x] is set

u is Element of (X,x,y)

z is Element of (X,x,y)

X is non empty being_B being_C being_I being_BCI-4 weakly-positive-implicative p-Semisimple BCIStr_0

the carrier of X is non empty set

0. X is V49(X) V142(X) positive nilpotent Element of the carrier of X

the ZeroF of X is Element of the carrier of X

y is Element of the carrier of X

z is Element of the carrier of X

u is Element of the carrier of X

x is Element of the carrier of X

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

the InternalDiff of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is Relation-like set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . ((0. X),x) is Element of the carrier of X

[(0. X),x] is set

the InternalDiff of X . [(0. X),x] is set

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

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

[u,((0. X) \ x)] is set

the InternalDiff of X . [u,((0. X) \ x)] is set

x2 is Element of the carrier of X

[: the carrier of X, the carrier of X:] is Relation-like set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

y is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

x is Element of the carrier of X

addLoopStr(# the carrier of X,y,x #) is strict addLoopStr

u is Element of the carrier of X

x is Element of the carrier of X

y . (u,x) is Element of the carrier of X

[u,x] is set

y . [u,x] is set

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

the InternalDiff of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

the InternalDiff of X . ((0. X),x) is Element of the carrier of X

[(0. X),x] is set

the InternalDiff of X . [(0. X),x] is set

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

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

[u,((0. X) \ x)] is set

the InternalDiff of X . [u,((0. X) \ x)] is set

x2 is Element of the carrier of X

c

(0. X) \ c

the InternalDiff of X . ((0. X),c

[(0. X),c

the InternalDiff of X . [(0. X),c

x2 \ ((0. X) \ c

the InternalDiff of X . (x2,((0. X) \ c

[x2,((0. X) \ c

the InternalDiff of X . [x2,((0. X) \ c

u is Element of the carrier of X

x is Element of the carrier of X

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

the InternalDiff of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

the InternalDiff of X . ((0. X),x) is Element of the carrier of X

[(0. X),x] is set

the InternalDiff of X . [(0. X),x] is set

x2 is Element of the carrier of X

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

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

[x2,((0. X) \ x)] is set

the InternalDiff of X . [x2,((0. X) \ x)] is set

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

the InternalDiff of X . ((0. X),x2) is Element of the carrier of X

[(0. X),x2] is set

the InternalDiff of X . [(0. X),x2] is set

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

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

[x,((0. X) \ x2)] is set

the InternalDiff of X . [x,((0. X) \ x2)] is set

x ` is Element of the carrier of X

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

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

the InternalDiff of X . ((0. X),(x `)) is Element of the carrier of X

[(0. X),(x `)] is set

the InternalDiff of X . [(0. X),(x `)] is set

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

the InternalDiff of X . (x,((x `) `)) is Element of the carrier of X

[x,((x `) `)] is set

the InternalDiff of X . [x,((x `) `)] is set

x \ x is Element of the carrier of X

the InternalDiff of X . (x,x) is Element of the carrier of X

[x,x] is set

the InternalDiff of X . [x,x] is set

the carrier of addLoopStr(# the carrier of X,y,x #) is set

u is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

x is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

u + x is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

the addF of addLoopStr(# the carrier of X,y,x #) is Relation-like Function-like V18([: the carrier of addLoopStr(# the carrier of X,y,x #), the carrier of addLoopStr(# the carrier of X,y,x #):], the carrier of addLoopStr(# the carrier of X,y,x #)) Element of bool [:[: the carrier of addLoopStr(# the carrier of X,y,x #), the carrier of addLoopStr(# the carrier of X,y,x #):], the carrier of addLoopStr(# the carrier of X,y,x #):]

[: the carrier of addLoopStr(# the carrier of X,y,x #), the carrier of addLoopStr(# the carrier of X,y,x #):] is Relation-like set

[:[: the carrier of addLoopStr(# the carrier of X,y,x #), the carrier of addLoopStr(# the carrier of X,y,x #):], the carrier of addLoopStr(# the carrier of X,y,x #):] is Relation-like set

bool [:[: the carrier of addLoopStr(# the carrier of X,y,x #), the carrier of addLoopStr(# the carrier of X,y,x #):], the carrier of addLoopStr(# the carrier of X,y,x #):] is set

the addF of addLoopStr(# the carrier of X,y,x #) . (u,x) is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

[u,x] is set

the addF of addLoopStr(# the carrier of X,y,x #) . [u,x] is set

x + u is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

the addF of addLoopStr(# the carrier of X,y,x #) . (x,u) is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

[x,u] is set

the addF of addLoopStr(# the carrier of X,y,x #) . [x,u] is set

x2 is Element of the carrier of X

c

(0. X) \ c

the InternalDiff of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

the InternalDiff of X . ((0. X),c

[(0. X),c

the InternalDiff of X . [(0. X),c

x2 \ ((0. X) \ c

the InternalDiff of X . (x2,((0. X) \ c

[x2,((0. X) \ c

the InternalDiff of X . [x2,((0. X) \ c

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

the InternalDiff of X . ((0. X),x2) is Element of the carrier of X

[(0. X),x2] is set

the InternalDiff of X . [(0. X),x2] is set

c

the InternalDiff of X . (c

[c

the InternalDiff of X . [c

the carrier of addLoopStr(# the carrier of X,y,x #) is set

u is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

x is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

x2 is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

u + x is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

the addF of addLoopStr(# the carrier of X,y,x #) is Relation-like Function-like V18([: the carrier of addLoopStr(# the carrier of X,y,x #), the carrier of addLoopStr(# the carrier of X,y,x #):], the carrier of addLoopStr(# the carrier of X,y,x #)) Element of bool [:[: the carrier of addLoopStr(# the carrier of X,y,x #), the carrier of addLoopStr(# the carrier of X,y,x #):], the carrier of addLoopStr(# the carrier of X,y,x #):]

[: the carrier of addLoopStr(# the carrier of X,y,x #), the carrier of addLoopStr(# the carrier of X,y,x #):] is Relation-like set

[:[: the carrier of addLoopStr(# the carrier of X,y,x #), the carrier of addLoopStr(# the carrier of X,y,x #):], the carrier of addLoopStr(# the carrier of X,y,x #):] is Relation-like set

bool [:[: the carrier of addLoopStr(# the carrier of X,y,x #), the carrier of addLoopStr(# the carrier of X,y,x #):], the carrier of addLoopStr(# the carrier of X,y,x #):] is set

the addF of addLoopStr(# the carrier of X,y,x #) . (u,x) is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

[u,x] is set

the addF of addLoopStr(# the carrier of X,y,x #) . [u,x] is set

(u + x) + x2 is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

the addF of addLoopStr(# the carrier of X,y,x #) . ((u + x),x2) is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

[(u + x),x2] is set

the addF of addLoopStr(# the carrier of X,y,x #) . [(u + x),x2] is set

c

y is Element of the carrier of X

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

the InternalDiff of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

the InternalDiff of X . ((0. X),y) is Element of the carrier of X

[(0. X),y] is set

the InternalDiff of X . [(0. X),y] is set

c

the InternalDiff of X . (c

[c

the InternalDiff of X . [c

z is Element of the carrier of X

y . ((c

[(c

y . [(c

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

the InternalDiff of X . ((0. X),z) is Element of the carrier of X

[(0. X),z] is set

the InternalDiff of X . [(0. X),z] is set

(c

the InternalDiff of X . ((c

[(c

the InternalDiff of X . [(c

(0. X) \ c

the InternalDiff of X . ((0. X),c

[(0. X),c

the InternalDiff of X . [(0. X),c

y \ ((0. X) \ c

the InternalDiff of X . (y,((0. X) \ c

[y,((0. X) \ c

the InternalDiff of X . [y,((0. X) \ c

(y \ ((0. X) \ c

the InternalDiff of X . ((y \ ((0. X) \ c

[(y \ ((0. X) \ c

the InternalDiff of X . [(y \ ((0. X) \ c

y \ ((0. X) \ z) is Element of the carrier of X

the InternalDiff of X . (y,((0. X) \ z)) is Element of the carrier of X

[y,((0. X) \ z)] is set

the InternalDiff of X . [y,((0. X) \ z)] is set

(y \ ((0. X) \ z)) \ ((0. X) \ c

the InternalDiff of X . ((y \ ((0. X) \ z)),((0. X) \ c

[(y \ ((0. X) \ z)),((0. X) \ c

the InternalDiff of X . [(y \ ((0. X) \ z)),((0. X) \ c

(0. X) \ (y \ ((0. X) \ z)) is Element of the carrier of X

the InternalDiff of X . ((0. X),(y \ ((0. X) \ z))) is Element of the carrier of X

[(0. X),(y \ ((0. X) \ z))] is set

the InternalDiff of X . [(0. X),(y \ ((0. X) \ z))] is set

c

the InternalDiff of X . (c

[c

the InternalDiff of X . [c

y . (c

[c

y . [c

x + x2 is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

the addF of addLoopStr(# the carrier of X,y,x #) . (x,x2) is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

[x,x2] is set

the addF of addLoopStr(# the carrier of X,y,x #) . [x,x2] is set

u + (x + x2) is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

the addF of addLoopStr(# the carrier of X,y,x #) . (u,(x + x2)) is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

[u,(x + x2)] is set

the addF of addLoopStr(# the carrier of X,y,x #) . [u,(x + x2)] is set

u is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

0. addLoopStr(# the carrier of X,y,x #) is V49( addLoopStr(# the carrier of X,y,x #)) Element of the carrier of addLoopStr(# the carrier of X,y,x #)

the ZeroF of addLoopStr(# the carrier of X,y,x #) is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

u + (0. addLoopStr(# the carrier of X,y,x #)) is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

the addF of addLoopStr(# the carrier of X,y,x #) . (u,(0. addLoopStr(# the carrier of X,y,x #))) is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

[u,(0. addLoopStr(# the carrier of X,y,x #))] is set

the addF of addLoopStr(# the carrier of X,y,x #) . [u,(0. addLoopStr(# the carrier of X,y,x #))] is set

x is Element of the carrier of X

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

the InternalDiff of X . ((0. X),(0. X)) is Element of the carrier of X

[(0. X),(0. X)] is set

the InternalDiff of X . [(0. X),(0. X)] is set

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

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

[x,((0. X) \ (0. X))] is set

the InternalDiff of X . [x,((0. X) \ (0. X))] is set

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

the InternalDiff of X . (x,(0. X)) is Element of the carrier of X

[x,(0. X)] is set

the InternalDiff of X . [x,(0. X)] is set

u is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

x is Element of the carrier of X

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

the InternalDiff of X . ((0. X),x) is Element of the carrier of X

[(0. X),x] is set

the InternalDiff of X . [(0. X),x] is set

x2 is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

u + x2 is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

the addF of addLoopStr(# the carrier of X,y,x #) . (u,x2) is Element of the carrier of addLoopStr(# the carrier of X,y,x #)

[u,x2] is set

the addF of addLoopStr(# the carrier of X,y,x #) . [u,x2] is set

c

c

the InternalDiff of X . (c

[c

the InternalDiff of X . [c

(0. X) \ c

the InternalDiff of X . ((0. X),c

[(0. X),c

the InternalDiff of X . [(0. X),c

x \ ((0. X) \ c

the InternalDiff of X . (x,((0. X) \ c

[x,((0. X) \ c

the InternalDiff of X . [x,((0. X) \ c

u is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr

the carrier of u is non empty set

the addF of u is Relation-like Function-like V18([: the carrier of u, the carrier of u:], the carrier of u) Element of bool [:[: the carrier of u, the carrier of u:], the carrier of u:]

[: the carrier of u, the carrier of u:] is Relation-like set

[:[: the carrier of u, the carrier of u:], the carrier of u:] is Relation-like set

bool [:[: the carrier of u, the carrier of u:], the carrier of u:] is set

0. u is V49(u) Element of the carrier of u

the ZeroF of u is Element of the carrier of u

x is Element of the carrier of X

x2 is Element of the carrier of X

the addF of u . (x,x2) is set

[x,x2] is set

the addF of u . [x,x2] is set

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

the InternalDiff of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

the InternalDiff of X . ((0. X),x2) is Element of the carrier of X

[(0. X),x2] is set

the InternalDiff of X . [(0. X),x2] is set

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

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

[x,((0. X) \ x2)] is set

the InternalDiff of X . [x,((0. X) \ x2)] is set

x is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr

the carrier of x is non empty set

the addF of x is Relation-like Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]

[: the carrier of x, the carrier of x:] is Relation-like set

[:[: the carrier of x, the carrier of x:], the carrier of x:] is Relation-like set

bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set

0. x is V49(x) Element of the carrier of x

the ZeroF of x is Element of the carrier of x

y is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr

the carrier of y is non empty set

the addF of y is Relation-like Function-like V18([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]

[: the carrier of y, the carrier of y:] is Relation-like set

[:[: the carrier of y, the carrier of y:], the carrier of y:] is Relation-like set

bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is set

0. y is V49(y) Element of the carrier of y

the ZeroF of y is Element of the carrier of y

z is Element of the carrier of x

u is Element of the carrier of x

the addF of x . (z,u) is Element of the carrier of x

[z,u] is set

the addF of x . [z,u] is set

x is Element of the carrier of X

x2 is Element of the carrier of X

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

the InternalDiff of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is Relation-like set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . ((0. X),x2) is Element of the carrier of X

[(0. X),x2] is set

the InternalDiff of X . [(0. X),x2] is set

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

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

[x,((0. X) \ x2)] is set

the InternalDiff of X . [x,((0. X) \ x2)] is set

the addF of y . (z,u) is set

the addF of y . [z,u] is set

X is non empty being_B being_C being_I being_BCI-4 BCIStr_0

the carrier of X is non empty set

0. X is V49(X) V142(X) positive nilpotent Element of the carrier of X

the ZeroF of X is Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

the InternalDiff of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is Relation-like set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . (x,y) is Element of the carrier of X

[x,y] is set

the InternalDiff of X . [x,y] is set

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

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

[(0. X),(x \ y)] is set

the InternalDiff of X . [(0. X),(x \ y)] is set

y \ x is Element of the carrier of X

the InternalDiff of X . (y,x) is Element of the carrier of X

[y,x] is set

the InternalDiff of X . [y,x] is set

(0. X) ` is Element of the carrier of X

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

the InternalDiff of X . ((0. X),(0. X)) is Element of the carrier of X

[(0. X),(0. X)] is set

the InternalDiff of X . [(0. X),(0. X)] is set

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

the InternalDiff of X . ((y \ x),((0. X) `)) is Element of the carrier of X

[(y \ x),((0. X) `)] is set

the InternalDiff of X . [(y \ x),((0. X) `)] is set

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

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

[(y \ x),(0. X)] is set

the InternalDiff of X . [(y \ x),(0. X)] is set

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

the InternalDiff of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is Relation-like set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . (x,y) is Element of the carrier of X

[x,y] is set

the InternalDiff of X . [x,y] is set

x is Element of the carrier of X

y is Element of the carrier of X

x \ y is Element of the carrier of X

the InternalDiff of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is Relation-like set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the InternalDiff of X . (x,y) is Element of the carrier of X

[x,y] is set

the InternalDiff of X . [x,y] is set

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

the InternalDiff of X . (x,(x \ y)) is Element of the carrier of X

[x,(x \ y)] is set

the InternalDiff of X . [x,(x \ y)] is set

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

the InternalDiff of X . ((x \ (x \ y)),y) is Element of the carrier of X

[(x \ (x \ y)),y] is set

the InternalDiff of X . [(x \ (x \ y)),y] is set

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

the InternalDiff of X . ((x \ y),(x \ y)) is Element of the carrier of X

[(x \ y),(x \ y)] is set

the InternalDiff of X . [(x \ y),(x \ y)] is set

X is non empty being_B being_C being_I being_BCI-4 () ()

the carrier of X is non empty set

0. X is V49(X) V142(X) positive nilpotent Element of the carrier of X

the ZeroF of X is Element of the carrier of X

x is Element of the carrier of X

y is Element of the carrier of X

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

the of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is Relation-like set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the of X . (x,y) is Element of the carrier of X

[x,y] is set

the of X . [x,y] is set

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

the InternalDiff of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

the InternalDiff of X . ((0. X),y) is Element of the carrier of X

[(0. X),y] is set

the InternalDiff of X . [(0. X),y] is set

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

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

[x,((0. X) \ y)] is set

the InternalDiff of X . [x,((0. X) \ y)] is set

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

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

[(x \ ((0. X) \ y)),x] is set

the InternalDiff of X . [(x \ ((0. X) \ y)),x] is set

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

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

[((x \ ((0. X) \ y)) \ x),y] is set

the InternalDiff of X . [((x \ ((0. X) \ y)) \ x),y] is set

x \ x is Element of the carrier of X

the InternalDiff of X . (x,x) is Element of the carrier of X

[x,x] is set

the InternalDiff of X . [x,x] is set

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

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

[(x \ x),((0. X) \ y)] is set

the InternalDiff of X . [(x \ x),((0. X) \ y)] is set

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

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

[((x \ x) \ ((0. X) \ y)),y] is set

the InternalDiff of X . [((x \ x) \ ((0. X) \ y)),y] is set

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

the InternalDiff of X . ((0. X),((0. X) \ y)) is Element of the carrier of X

[(0. X),((0. X) \ y)] is set

the InternalDiff of X . [(0. X),((0. X) \ y)] is set

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

the InternalDiff of X . (((0. X) \ ((0. X) \ y)),y) is Element of the carrier of X

[((0. X) \ ((0. X) \ y)),y] is set

the InternalDiff of X . [((0. X) \ ((0. X) \ y)),y] is set

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

the InternalDiff of X . (((0. X) \ y),((0. X) \ y)) is Element of the carrier of X

[((0. X) \ y),((0. X) \ y)] is set

the InternalDiff of X . [((0. X) \ y),((0. X) \ y)] is set

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

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

[(x \ ((0. X) \ y)),(X,x,y)] is set

the InternalDiff of X . [(x \ ((0. X) \ y)),(X,x,y)] is set

x is Element of the carrier of X

x \ x is Element of the carrier of X

the InternalDiff of X . (x,x) is Element of the carrier of X

[x,x] is set

the InternalDiff of X . [x,x] is set

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

the InternalDiff of X . ((x \ x),y) is Element of the carrier of X

[(x \ x),y] is set

the InternalDiff of X . [(x \ x),y] is set

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

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

[x,(x \ ((0. X) \ y))] is set

the InternalDiff of X . [x,(x \ ((0. X) \ y))] is set

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

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

[(0. X),(x \ x)] is set

the InternalDiff of X . [(0. X),(x \ x)] is set

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

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

[x,((0. X) \ (x \ x))] is set

the InternalDiff of X . [x,((0. X) \ (x \ x))] is set

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

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

[x,(x \ ((0. X) \ (x \ x)))] is set

the InternalDiff of X . [x,(x \ ((0. X) \ (x \ x)))] is set

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

the InternalDiff of X . (x,(0. X)) is Element of the carrier of X

[x,(0. X)] is set

the InternalDiff of X . [x,(0. X)] is set

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

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

[x,(x \ (0. X))] is set

the InternalDiff of X . [x,(x \ (0. X))] is set

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

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

[x,(x \ (x \ (0. X)))] is set

the InternalDiff of X . [x,(x \ (x \ (0. X)))] is set

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

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

[x,(x \ (x \ (x \ (0. X))))] is set

the InternalDiff of X . [x,(x \ (x \ (x \ (0. X))))] is set

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

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

[x,(x \ (0. X))] is set

the InternalDiff of X . [x,(x \ (0. X))] is set

x \ x is Element of the carrier of X

the InternalDiff of X . (x,x) is Element of the carrier of X

[x,x] is set

the InternalDiff of X . [x,x] is set

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

the InternalDiff of X . ((X,x,y),x) is Element of the carrier of X

[(X,x,y),x] is set

the InternalDiff of X . [(X,x,y),x] is set

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

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

[(X,x,y),(x \ ((0. X) \ y))] is set

the InternalDiff of X . [(X,x,y),(x \ ((0. X) \ y))] is set

x is Element of the carrier of X

y is Element of the carrier of X

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

the of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is Relation-like set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the of X . (x,y) is Element of the carrier of X

[x,y] is set

the of X . [x,y] is set

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

the InternalDiff of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

the InternalDiff of X . ((0. X),y) is Element of the carrier of X

[(0. X),y] is set

the InternalDiff of X . [(0. X),y] is set

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

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

[x,((0. X) \ y)] is set

the InternalDiff of X . [x,((0. X) \ y)] is set

X is non empty being_B being_C being_I being_BCI-4 () ()

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) is Element of the carrier of X

the of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is Relation-like set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is set

the of X . (x,y) is Element of the carrier of X

[x,y] is set

the of X . [x,y] is set

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

the of X . (y,x) is Element of the carrier of X

[y,x] is set

the of X . [y,x] is set

(X,y,