:: BCIALG_4 semantic presentation

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

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
{ b1 where b1 is V24() V25() V26() V30() V33() V38() ext-real Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
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
{ b1 where b1 is Element of the carrier of X : b1 \ x <= y } is set
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
{ b1 where b1 is Element of the carrier of X : b1 \ x <= y } is set
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
{ b1 where b1 is Element of the carrier of X : b1 \ x <= y } is set
(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
{ b1 where b1 is Element of the carrier of X : b1 \ x <= y } is set
(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)

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
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
c8 is Element of the carrier of X
(0. X) \ c8 is Element of the carrier of X
the InternalDiff of X . ((0. X),c8) is Element of the carrier of X
[(0. X),c8] is set
the InternalDiff of X . [(0. X),c8] is set
x2 \ ((0. X) \ c8) is Element of the carrier of X
the InternalDiff of X . (x2,((0. X) \ c8)) is Element of the carrier of X
[x2,((0. X) \ c8)] is set
the InternalDiff of X . [x2,((0. X) \ c8)] is set
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
c8 is Element of the carrier of X
(0. X) \ c8 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),c8) is Element of the carrier of X
[(0. X),c8] is set
the InternalDiff of X . [(0. X),c8] is set
x2 \ ((0. X) \ c8) is Element of the carrier of X
the InternalDiff of X . (x2,((0. X) \ c8)) is Element of the carrier of X
[x2,((0. X) \ c8)] is set
the InternalDiff of X . [x2,((0. X) \ c8)] 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
c8 \ ((0. X) \ x2) is Element of the carrier of X
the InternalDiff of X . (c8,((0. X) \ x2)) is Element of the carrier of X
[c8,((0. X) \ x2)] is set
the InternalDiff of X . [c8,((0. X) \ x2)] 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 #)
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
c8 is Element of the carrier of X
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
c8 \ ((0. X) \ y) is Element of the carrier of X
the InternalDiff of X . (c8,((0. X) \ y)) is Element of the carrier of X
[c8,((0. X) \ y)] is set
the InternalDiff of X . [c8,((0. X) \ y)] is set
z is Element of the carrier of X
y . ((c8 \ ((0. X) \ y)),z) is Element of the carrier of X
[(c8 \ ((0. X) \ y)),z] is set
y . [(c8 \ ((0. X) \ y)),z] is set
(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
(c8 \ ((0. X) \ y)) \ ((0. X) \ z) is Element of the carrier of X
the InternalDiff of X . ((c8 \ ((0. X) \ y)),((0. X) \ z)) is Element of the carrier of X
[(c8 \ ((0. X) \ y)),((0. X) \ z)] is set
the InternalDiff of X . [(c8 \ ((0. X) \ y)),((0. X) \ z)] is set
(0. X) \ c8 is Element of the carrier of X
the InternalDiff of X . ((0. X),c8) is Element of the carrier of X
[(0. X),c8] is set
the InternalDiff of X . [(0. X),c8] is set
y \ ((0. X) \ c8) is Element of the carrier of X
the InternalDiff of X . (y,((0. X) \ c8)) is Element of the carrier of X
[y,((0. X) \ c8)] is set
the InternalDiff of X . [y,((0. X) \ c8)] is set
(y \ ((0. X) \ c8)) \ ((0. X) \ z) is Element of the carrier of X
the InternalDiff of X . ((y \ ((0. X) \ c8)),((0. X) \ z)) is Element of the carrier of X
[(y \ ((0. X) \ c8)),((0. X) \ z)] is set
the InternalDiff of X . [(y \ ((0. X) \ c8)),((0. X) \ z)] is set
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) \ c8) is Element of the carrier of X
the InternalDiff of X . ((y \ ((0. X) \ z)),((0. X) \ c8)) is Element of the carrier of X
[(y \ ((0. X) \ z)),((0. X) \ c8)] is set
the InternalDiff of X . [(y \ ((0. X) \ z)),((0. X) \ c8)] is set
(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
c8 \ ((0. X) \ (y \ ((0. X) \ z))) is Element of the carrier of X
the InternalDiff of X . (c8,((0. X) \ (y \ ((0. X) \ z)))) is Element of the carrier of X
[c8,((0. X) \ (y \ ((0. X) \ z)))] is set
the InternalDiff of X . [c8,((0. X) \ (y \ ((0. X) \ z)))] is set
y . (c8,(y \ ((0. X) \ z))) is Element of the carrier of X
[c8,(y \ ((0. X) \ z))] is set
y . [c8,(y \ ((0. X) \ z))] is set
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
c8 is Element of the carrier of X
c8 \ ((0. X) \ x) is Element of the carrier of X
the InternalDiff of X . (c8,((0. X) \ x)) is Element of the carrier of X
[c8,((0. X) \ x)] is set
the InternalDiff of X . [c8,((0. X) \ x)] is set
(0. X) \ c8 is Element of the carrier of X
the InternalDiff of X . ((0. X),c8) is Element of the carrier of X
[(0. X),c8] is set
the InternalDiff of X . [(0. X),c8] is set
x \ ((0. X) \ c8) is Element of the carrier of X
the InternalDiff of X . (x,((0. X) \ c8)) is Element of the carrier of X
[x,((0. X) \ c8)] is set
the InternalDiff of X . [x,((0. X) \ c8)] is set

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

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

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

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,