REAL is set
NAT is non empty V21() V22() V23() Element of bool REAL
bool REAL is non empty set
NAT is non empty V21() V22() V23() set
bool NAT is non empty set
COMPLEX is set
RAT is set
INT is set
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty set
[:[:NAT,NAT:],NAT:] is non empty set
bool [:[:NAT,NAT:],NAT:] is non empty set
bool NAT is non empty set
K273() is set
1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
{} is set
the empty V21() V22() V23() V25() V26() V27() V74() ext-real non negative V78() set is empty V21() V22() V23() V25() V26() V27() V74() ext-real non negative V78() set
0 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
I is Element of the carrier of X
RI is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is Element of the carrier of X
x1 is Element of the carrier of X
x1 is Element of the carrier of X
y1 is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
y1 . w1 is Element of the carrier of X
y1 . 0 is Element of the carrier of X
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(y1 . w1) \ x1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((y1 . w1),x1) is Element of the carrier of X
y1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
y1 . x1 is set
y1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
j is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
z1 is Element of the carrier of X
y1 . x1 is Element of the carrier of X
j is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
z1 is Element of the carrier of X
z1 is Element of the carrier of X
j is Element of the carrier of X
x1 is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
x1 . (w1 + 1) is Element of the carrier of X
y1 is Element of the carrier of X
z1 is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
z1 . (w1 + 1) is Element of the carrier of X
z1 . 0 is Element of the carrier of X
j is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
j + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
y1 . (j + 1) is Element of the carrier of X
y1 . j is Element of the carrier of X
(y1 . j) \ x1 is Element of the carrier of X
the InternalDiff of X . ((y1 . j),x1) is Element of the carrier of X
x1 . j is Element of the carrier of X
(x1 . j) \ x1 is Element of the carrier of X
the InternalDiff of X . ((x1 . j),x1) is Element of the carrier of X
z1 . (j + 1) is Element of the carrier of X
z1 . j is Element of the carrier of X
(z1 . j) \ x1 is Element of the carrier of X
the InternalDiff of X . ((z1 . j),x1) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
y1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is Element of the carrier of X
x1 is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 is Element of the carrier of X
NAT --> w1 is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) V25() Element of bool [:NAT, the carrier of X:]
y1 is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
y1 . x1 is Element of the carrier of X
x1 is Element of the carrier of X
y1 is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
y1 . x1 is Element of the carrier of X
y1 . 0 is Element of the carrier of X
x1 is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
y1 . (x1 + 1) is Element of the carrier of X
y1 . x1 is Element of the carrier of X
(y1 . x1) \ x1 is Element of the carrier of X
the InternalDiff of X . ((y1 . x1),x1) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 is Element of the carrier of X
x1 is Element of the carrier of X
w1 is Element of the carrier of X
x1 is Element of the carrier of X
x1 is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
x1 . IT is Element of the carrier of X
x1 . 0 is Element of the carrier of X
y1 is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
y1 . IT is Element of the carrier of X
y1 . 0 is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 . x1 is Element of the carrier of X
y1 . x1 is Element of the carrier of X
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 . (x1 + 1) is Element of the carrier of X
(x1 . x1) \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((x1 . x1),RI) is Element of the carrier of X
y1 . (x1 + 1) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 . x1 is Element of the carrier of X
y1 . x1 is Element of the carrier of X
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 . (x1 + 1) is Element of the carrier of X
y1 . (x1 + 1) is Element of the carrier of X
x1 . 0 is Element of the carrier of X
y1 . 0 is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
(X,I,RI,0) is Element of the carrier of X
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
IT is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
IT . 0 is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
(X,I,RI,1) is Element of the carrier of X
I \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (I,RI) is Element of the carrier of X
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
IT is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
IT . 1 is Element of the carrier of X
IT . 0 is Element of the carrier of X
0 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT . (0 + 1) is Element of the carrier of X
2 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
(X,I,RI,2) is Element of the carrier of X
I \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (I,RI) is Element of the carrier of X
(I \ RI) \ RI is Element of the carrier of X
the InternalDiff of X . ((I \ RI),RI) is Element of the carrier of X
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
IT is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
IT . 2 is Element of the carrier of X
IT . 0 is Element of the carrier of X
1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT . (1 + 1) is Element of the carrier of X
0 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT . (0 + 1) is Element of the carrier of X
(IT . (0 + 1)) \ RI is Element of the carrier of X
the InternalDiff of X . ((IT . (0 + 1)),RI) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,(IT + 1)) is Element of the carrier of X
(X,I,RI,IT) is Element of the carrier of X
(X,I,RI,IT) \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((X,I,RI,IT),RI) is Element of the carrier of X
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
w1 is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
w1 . IT is Element of the carrier of X
w1 . 0 is Element of the carrier of X
x1 is Relation-like NAT -defined the carrier of X -valued Function-like V18( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
x1 . (IT + 1) is Element of the carrier of X
x1 . 0 is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
y1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 . (x1 + 1) is Element of the carrier of X
x1 . x1 is Element of the carrier of X
(x1 . x1) \ RI is Element of the carrier of X
the InternalDiff of X . ((x1 . x1),RI) is Element of the carrier of X
w1 . (x1 + 1) is Element of the carrier of X
w1 . x1 is Element of the carrier of X
(w1 . x1) \ RI is Element of the carrier of X
the InternalDiff of X . ((w1 . x1),RI) is Element of the carrier of X
x1 . y1 is Element of the carrier of X
w1 . y1 is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
y1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 . y1 is Element of the carrier of X
w1 . y1 is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 . x1 is Element of the carrier of X
w1 . x1 is Element of the carrier of X
x1 . IT is Element of the carrier of X
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 V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
RI + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(0. X),(RI + 1)) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(0. X),(w1 + 1)) is Element of the carrier of X
(X,I,(0. X),(IT + 1)) is Element of the carrier of X
(X,I,(0. X),(IT + 1)) \ (0. X) is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((X,I,(0. X),(IT + 1)),(0. X)) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(0. X),(w1 + 1)) is Element of the carrier of X
0 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(0. X),(0 + 1)) is Element of the carrier of X
I \ (0. X) is Element of the carrier of X
the InternalDiff of X . (I,(0. X)) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(0. X),(IT + 1)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
0. X is V44(X) Element of the carrier of X
the carrier of X is non empty set
the ZeroF of X is Element of the carrier of X
I is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(0. X),I) is Element of the carrier of X
RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
RI + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(0. X),IT) is Element of the carrier of X
RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(0. X),RI) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
IT is Element of the carrier of X
I \ IT is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (I,IT) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,w1) is Element of the carrier of X
(X,I,RI,w1) \ IT is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,w1),IT) is Element of the carrier of X
(X,(I \ IT),RI,w1) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,x1) is Element of the carrier of X
(X,I,RI,x1) \ IT is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,x1),IT) is Element of the carrier of X
(X,I,RI,x1) is Element of the carrier of X
(X,I,RI,x1) \ RI is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,x1),RI) is Element of the carrier of X
((X,I,RI,x1) \ RI) \ IT is Element of the carrier of X
the InternalDiff of X . (((X,I,RI,x1) \ RI),IT) is Element of the carrier of X
(X,I,RI,x1) \ IT is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,x1),IT) is Element of the carrier of X
((X,I,RI,x1) \ IT) \ RI is Element of the carrier of X
the InternalDiff of X . (((X,I,RI,x1) \ IT),RI) is Element of the carrier of X
(X,(I \ IT),RI,x1) is Element of the carrier of X
(X,(I \ IT),RI,x1) \ RI is Element of the carrier of X
the InternalDiff of X . ((X,(I \ IT),RI,x1),RI) is Element of the carrier of X
(X,(I \ IT),RI,(x1 + 1)) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,x1) is Element of the carrier of X
(X,I,RI,x1) \ IT is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,x1),IT) is Element of the carrier of X
(X,(I \ IT),RI,x1) is Element of the carrier of X
(X,I,RI,0) is Element of the carrier of X
(X,I,RI,0) \ IT is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,0),IT) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,x1) is Element of the carrier of X
(X,I,RI,x1) \ IT is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,x1),IT) is Element of the carrier of X
(X,(I \ IT),RI,x1) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
I \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (I,RI) is Element of the carrier of X
I \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . (I,(I \ RI)) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(I \ (I \ RI)),IT) is Element of the carrier of X
(X,I,RI,IT) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(I \ (I \ RI)),(w1 + 1)) is Element of the carrier of X
(X,I,(I \ (I \ RI)),w1) is Element of the carrier of X
(X,I,(I \ (I \ RI)),w1) \ (I \ (I \ RI)) is Element of the carrier of X
the InternalDiff of X . ((X,I,(I \ (I \ RI)),w1),(I \ (I \ RI))) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,w1) is Element of the carrier of X
(X,I,RI,w1) \ (I \ (I \ RI)) is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,w1),(I \ (I \ RI))) is Element of the carrier of X
I \ (I \ (I \ RI)) is Element of the carrier of X
the InternalDiff of X . (I,(I \ (I \ RI))) is Element of the carrier of X
(X,(I \ (I \ (I \ RI))),RI,w1) is Element of the carrier of X
(X,(I \ RI),RI,w1) is Element of the carrier of X
(X,I,RI,w1) \ RI is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,w1),RI) is Element of the carrier of X
(X,I,RI,(w1 + 1)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(I \ (I \ RI)),x1) is Element of the carrier of X
(X,I,RI,x1) is Element of the carrier of X
(X,I,(I \ (I \ RI)),0) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(I \ (I \ RI)),w1) is Element of the carrier of X
(X,I,RI,w1) is Element of the carrier of X
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 V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
I ` is Element of the carrier of X
(0. X) \ I is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),I) is Element of the carrier of X
RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,RI) is Element of the carrier of X
(X,(0. X),I,RI) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,RI) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,RI)) is Element of the carrier of X
(X,(0. X),(I `),RI) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(IT + 1)) is Element of the carrier of X
(X,(0. X),I,(IT + 1)) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,(IT + 1)) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,(IT + 1))) is Element of the carrier of X
(X,(0. X),I,IT) is Element of the carrier of X
(X,(0. X),I,IT) \ I is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,IT),I) is Element of the carrier of X
((X,(0. X),I,IT) \ I) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,IT) \ I) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,IT) \ I)) is Element of the carrier of X
(X,(0. X),I,IT) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,IT) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,IT)) is Element of the carrier of X
((X,(0. X),I,IT) `) \ (I `) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,IT) `),(I `)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(I `),IT) is Element of the carrier of X
(X,(0. X),(I `),IT) \ (I `) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),(I `),IT),(I `)) is Element of the carrier of X
(X,(0. X),(I `),(IT + 1)) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,w1) is Element of the carrier of X
(X,(0. X),I,w1) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,w1) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,w1)) is Element of the carrier of X
(X,(0. X),(I `),w1) is Element of the carrier of X
(X,(0. X),I,0) is Element of the carrier of X
(X,(0. X),I,0) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,0) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,0)) is Element of the carrier of X
(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
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,IT) is Element of the carrier of X
(X,(0. X),I,IT) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,IT) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,IT)) is Element of the carrier of X
(X,(0. X),(I `),IT) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,IT) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(X,I,RI,IT),RI,w1) is Element of the carrier of X
IT + w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,(IT + w1)) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,x1) is Element of the carrier of X
(X,(X,I,RI,x1),RI,w1) is Element of the carrier of X
x1 + w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,(x1 + w1)) is Element of the carrier of X
(X,(X,I,RI,x1),RI,w1) \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((X,(X,I,RI,x1),RI,w1),RI) is Element of the carrier of X
(x1 + w1) + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,((x1 + w1) + 1)) is Element of the carrier of X
(X,I,RI,x1) \ RI is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,x1),RI) is Element of the carrier of X
(X,((X,I,RI,x1) \ RI),RI,w1) is Element of the carrier of X
(X,I,RI,x1) is Element of the carrier of X
(X,(X,I,RI,x1),RI,w1) is Element of the carrier of X
x1 + w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,(x1 + w1)) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,x1) is Element of the carrier of X
(X,(X,I,RI,x1),RI,w1) is Element of the carrier of X
x1 + w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,(x1 + w1)) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,x1) is Element of the carrier of X
(X,(X,I,RI,x1),RI,w1) is Element of the carrier of X
x1 + w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,(x1 + w1)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
IT is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,w1) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(X,I,RI,w1),IT,x1) is Element of the carrier of X
(X,I,IT,x1) is Element of the carrier of X
(X,(X,I,IT,x1),RI,w1) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
y1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,x1) is Element of the carrier of X
(X,(X,I,RI,x1),IT,x1) is Element of the carrier of X
(X,(X,I,RI,x1),IT,x1) \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((X,(X,I,RI,x1),IT,x1),RI) is Element of the carrier of X
(X,(X,I,IT,x1),RI,x1) is Element of the carrier of X
(X,(X,I,IT,x1),RI,x1) \ RI is Element of the carrier of X
the InternalDiff of X . ((X,(X,I,IT,x1),RI,x1),RI) is Element of the carrier of X
(X,(X,I,IT,x1),RI,(x1 + 1)) is Element of the carrier of X
(X,I,RI,x1) \ RI is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,x1),RI) is Element of the carrier of X
(X,((X,I,RI,x1) \ RI),IT,x1) is Element of the carrier of X
(X,I,RI,(x1 + 1)) is Element of the carrier of X
(X,(X,I,RI,(x1 + 1)),IT,x1) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
y1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,y1) is Element of the carrier of X
(X,(X,I,RI,y1),IT,x1) is Element of the carrier of X
(X,(X,I,IT,x1),RI,y1) is Element of the carrier of X
(X,I,RI,0) is Element of the carrier of X
(X,(X,I,RI,0),IT,x1) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,x1) is Element of the carrier of X
(X,(X,I,RI,x1),IT,x1) is Element of the carrier of X
(X,(X,I,IT,x1),RI,x1) is Element of the carrier of X
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 V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,RI) is Element of the carrier of X
(X,(0. X),I,RI) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,RI) is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),(X,(0. X),I,RI)) is Element of the carrier of X
((X,(0. X),I,RI) `) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,RI) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,RI) `)) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(IT + 1)) is Element of the carrier of X
(X,(0. X),I,(IT + 1)) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,(IT + 1)) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,(IT + 1))) is Element of the carrier of X
((X,(0. X),I,(IT + 1)) `) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,(IT + 1)) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,(IT + 1)) `)) is Element of the carrier of X
(X,(0. X),I,IT) is Element of the carrier of X
(X,(0. X),I,IT) \ I is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,IT),I) is Element of the carrier of X
((X,(0. X),I,IT) \ I) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,IT) \ I) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,IT) \ I)) is Element of the carrier of X
(((X,(0. X),I,IT) \ I) `) ` is Element of the carrier of X
(0. X) \ (((X,(0. X),I,IT) \ I) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),(((X,(0. X),I,IT) \ I) `)) is Element of the carrier of X
(X,(0. X),I,IT) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,IT) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,IT)) is Element of the carrier of X
I ` is Element of the carrier of X
(0. X) \ I is Element of the carrier of X
the InternalDiff of X . ((0. X),I) is Element of the carrier of X
((X,(0. X),I,IT) `) \ (I `) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,IT) `),(I `)) is Element of the carrier of X
(((X,(0. X),I,IT) `) \ (I `)) ` is Element of the carrier of X
(0. X) \ (((X,(0. X),I,IT) `) \ (I `)) is Element of the carrier of X
the InternalDiff of X . ((0. X),(((X,(0. X),I,IT) `) \ (I `))) is Element of the carrier of X
((X,(0. X),I,IT) `) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,IT) `)) is Element of the carrier of X
(I `) ` is Element of the carrier of X
(0. X) \ (I `) is Element of the carrier of X
the InternalDiff of X . ((0. X),(I `)) is Element of the carrier of X
(((X,(0. X),I,IT) `) `) \ ((I `) `) is Element of the carrier of X
the InternalDiff of X . ((((X,(0. X),I,IT) `) `),((I `) `)) is Element of the carrier of X
(X,(0. X),I,IT) \ ((I `) `) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,IT),((I `) `)) is Element of the carrier of X
((I `) `) ` is Element of the carrier of X
(0. X) \ ((I `) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((I `) `)) is Element of the carrier of X
(X,(((I `) `) `),I,IT) is Element of the carrier of X
(X,(I `),I,IT) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
IT + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,w1) is Element of the carrier of X
(X,(0. X),I,w1) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,w1) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,w1)) is Element of the carrier of X
((X,(0. X),I,w1) `) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,w1) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,w1) `)) is Element of the carrier of X
(X,(0. X),I,0) is Element of the carrier of X
(X,(0. X),I,0) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,0) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,0)) is Element of the carrier of X
((X,(0. X),I,0) `) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,0) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,0) `)) is Element of the carrier of X
(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) `) ` 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
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,IT) is Element of the carrier of X
(X,(0. X),I,IT) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,IT) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,IT)) is Element of the carrier of X
((X,(0. X),I,IT) `) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,IT) `)) is Element of the carrier of X
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 V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,RI) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
RI + IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI + IT)) is Element of the carrier of X
(X,(0. X),I,IT) is Element of the carrier of X
(X,(0. X),I,IT) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,IT) is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),(X,(0. X),I,IT)) is Element of the carrier of X
(X,(0. X),I,RI) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,RI),((X,(0. X),I,IT) `)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(w1 + IT) + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,((w1 + IT) + 1)) is Element of the carrier of X
(X,(0. X),I,(w1 + IT)) is Element of the carrier of X
(X,(0. X),I,(w1 + IT)) \ I is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,(w1 + IT)),I) is Element of the carrier of X
(X,(0. X),I,w1) is Element of the carrier of X
(X,(0. X),I,w1) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,w1),((X,(0. X),I,IT) `)) is Element of the carrier of X
((X,(0. X),I,w1) \ ((X,(0. X),I,IT) `)) \ I is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,w1) \ ((X,(0. X),I,IT) `)),I) is Element of the carrier of X
(X,(0. X),I,w1) \ I is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,w1),I) is Element of the carrier of X
((X,(0. X),I,w1) \ I) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,w1) \ I),((X,(0. X),I,IT) `)) is Element of the carrier of X
(w1 + 1) + IT is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,((w1 + 1) + IT)) is Element of the carrier of X
(X,(0. X),I,(w1 + 1)) is Element of the carrier of X
(X,(0. X),I,(w1 + 1)) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,(w1 + 1)),((X,(0. X),I,IT) `)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(x1 + IT)) is Element of the carrier of X
(X,(0. X),I,x1) is Element of the carrier of X
(X,(0. X),I,x1) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,x1),((X,(0. X),I,IT) `)) is Element of the carrier of X
0 + IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(0 + IT)) is Element of the carrier of X
((X,(0. X),I,IT) `) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,IT) `)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(w1 + IT)) is Element of the carrier of X
(X,(0. X),I,w1) is Element of the carrier of X
(X,(0. X),I,w1) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,w1),((X,(0. X),I,IT) `)) is Element of the carrier of X
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 V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,RI) is Element of the carrier of X
(X,(0. X),I,RI) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,RI) is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),(X,(0. X),I,RI)) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
RI + IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI + IT)) is Element of the carrier of X
(X,(0. X),I,(RI + IT)) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,(RI + IT)) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,(RI + IT))) is Element of the carrier of X
(X,(0. X),I,IT) is Element of the carrier of X
((X,(0. X),I,RI) `) \ (X,(0. X),I,IT) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,RI) `),(X,(0. X),I,IT)) is Element of the carrier of X
(X,(0. X),I,IT) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,IT) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,IT)) is Element of the carrier of X
(X,(0. X),I,RI) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,RI),((X,(0. X),I,IT) `)) is Element of the carrier of X
((X,(0. X),I,RI) \ ((X,(0. X),I,IT) `)) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,RI) \ ((X,(0. X),I,IT) `)) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,RI) \ ((X,(0. X),I,IT) `))) is Element of the carrier of X
((X,(0. X),I,IT) `) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,IT) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,IT) `)) is Element of the carrier of X
((X,(0. X),I,RI) `) \ (((X,(0. X),I,IT) `) `) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,RI) `),(((X,(0. X),I,IT) `) `)) is Element of the carrier of X
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 V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,RI) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(X,(0. X),I,RI),IT) is Element of the carrier of X
(X,(0. X),(X,(0. X),I,RI),IT) ` is Element of the carrier of X
(0. X) \ (X,(0. X),(X,(0. X),I,RI),IT) is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),(X,(0. X),(X,(0. X),I,RI),IT)) is Element of the carrier of X
RI * IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI * IT)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(X,(0. X),I,RI),(w1 + 1)) is Element of the carrier of X
(X,(0. X),(X,(0. X),I,RI),(w1 + 1)) ` is Element of the carrier of X
(0. X) \ (X,(0. X),(X,(0. X),I,RI),(w1 + 1)) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),(X,(0. X),I,RI),(w1 + 1))) is Element of the carrier of X
(X,(0. X),(X,(0. X),I,RI),w1) is Element of the carrier of X
(X,(0. X),(X,(0. X),I,RI),w1) \ (X,(0. X),I,RI) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),(X,(0. X),I,RI),w1),(X,(0. X),I,RI)) is Element of the carrier of X
((X,(0. X),(X,(0. X),I,RI),w1) \ (X,(0. X),I,RI)) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),(X,(0. X),I,RI),w1) \ (X,(0. X),I,RI)) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),(X,(0. X),I,RI),w1) \ (X,(0. X),I,RI))) is Element of the carrier of X
(X,(0. X),(X,(0. X),I,RI),w1) ` is Element of the carrier of X
(0. X) \ (X,(0. X),(X,(0. X),I,RI),w1) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),(X,(0. X),I,RI),w1)) is Element of the carrier of X
(X,(0. X),I,RI) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,RI) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,RI)) is Element of the carrier of X
((X,(0. X),(X,(0. X),I,RI),w1) `) \ ((X,(0. X),I,RI) `) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),(X,(0. X),I,RI),w1) `),((X,(0. X),I,RI) `)) is Element of the carrier of X
RI * w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI * w1)) is Element of the carrier of X
(X,(0. X),I,(RI * w1)) \ ((X,(0. X),I,RI) `) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,(RI * w1)),((X,(0. X),I,RI) `)) is Element of the carrier of X
(RI * w1) + RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,((RI * w1) + RI)) is Element of the carrier of X
RI * (w1 + 1) is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI * (w1 + 1))) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(X,(0. X),I,RI),x1) is Element of the carrier of X
(X,(0. X),(X,(0. X),I,RI),x1) ` is Element of the carrier of X
(0. X) \ (X,(0. X),(X,(0. X),I,RI),x1) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),(X,(0. X),I,RI),x1)) is Element of the carrier of X
RI * x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI * x1)) is Element of the carrier of X
(X,(0. X),(X,(0. X),I,RI),0) is Element of the carrier of X
(X,(0. X),(X,(0. X),I,RI),0) ` is Element of the carrier of X
(0. X) \ (X,(0. X),(X,(0. X),I,RI),0) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),(X,(0. X),I,RI),0)) is Element of the carrier of X
(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
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(X,(0. X),I,RI),w1) is Element of the carrier of X
(X,(0. X),(X,(0. X),I,RI),w1) ` is Element of the carrier of X
(0. X) \ (X,(0. X),(X,(0. X),I,RI),w1) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),(X,(0. X),I,RI),w1)) is Element of the carrier of X
RI * w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI * w1)) is Element of the carrier of X
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 V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,RI) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
RI * IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI * IT)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
RI * (w1 + 1) is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI * (w1 + 1))) is Element of the carrier of X
RI * w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(RI * w1) + RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,((RI * w1) + RI)) is Element of the carrier of X
(X,(0. X),I,(RI * w1)) is Element of the carrier of X
(X,(X,(0. X),I,(RI * w1)),I,RI) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
RI * x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI * x1)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
RI * w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,(RI * w1)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
I \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (I,RI) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,IT) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,(w1 + 1)) is Element of the carrier of X
(X,I,RI,w1) is Element of the carrier of X
(X,I,RI,w1) \ RI is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,w1),RI) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,x1) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,w1) is Element of the carrier of X
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 V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
RI is Element of the carrier of X
I \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (I,RI) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(I \ RI),IT) is Element of the carrier of X
(X,(0. X),I,IT) is Element of the carrier of X
(X,(0. X),RI,IT) is Element of the carrier of X
(X,(0. X),I,IT) \ (X,(0. X),RI,IT) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,IT),(X,(0. X),RI,IT)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(I \ RI),x1) is Element of the carrier of X
(X,(0. X),I,x1) is Element of the carrier of X
(X,(0. X),RI,x1) is Element of the carrier of X
(X,(0. X),I,x1) \ (X,(0. X),RI,x1) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,x1),(X,(0. X),RI,x1)) is Element of the carrier of X
(X,(0. X),(I \ RI),w1) is Element of the carrier of X
(X,(0. X),I,w1) is Element of the carrier of X
(X,(0. X),RI,w1) is Element of the carrier of X
(X,(0. X),I,w1) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,w1),(X,(0. X),RI,w1)) is Element of the carrier of X
(X,(0. X),(I \ RI),(w1 + 1)) is Element of the carrier of X
((X,(0. X),I,w1) \ (X,(0. X),RI,w1)) \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,w1) \ (X,(0. X),RI,w1)),(I \ RI)) is Element of the carrier of X
(X,(0. X),I,w1) \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,w1),(I \ RI)) is Element of the carrier of X
((X,(0. X),I,w1) \ (I \ RI)) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,w1) \ (I \ RI)),(X,(0. X),RI,w1)) is Element of the carrier of X
(I \ RI) ` is Element of the carrier of X
(0. X) \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . ((0. X),(I \ RI)) is Element of the carrier of X
(X,((I \ RI) `),I,w1) is Element of the carrier of X
(X,((I \ RI) `),I,w1) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . ((X,((I \ RI) `),I,w1),(X,(0. X),RI,w1)) is Element of the carrier of X
I ` is Element of the carrier of X
(0. X) \ I is Element of the carrier of X
the InternalDiff of X . ((0. X),I) is Element of the carrier of X
RI ` is Element of the carrier of X
(0. X) \ RI is Element of the carrier of X
the InternalDiff of X . ((0. X),RI) is Element of the carrier of X
(I `) \ (RI `) is Element of the carrier of X
the InternalDiff of X . ((I `),(RI `)) is Element of the carrier of X
(X,((I `) \ (RI `)),I,w1) is Element of the carrier of X
(X,((I `) \ (RI `)),I,w1) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . ((X,((I `) \ (RI `)),I,w1),(X,(0. X),RI,w1)) is Element of the carrier of X
(X,(I `),I,w1) is Element of the carrier of X
(X,(I `),I,w1) \ (RI `) is Element of the carrier of X
the InternalDiff of X . ((X,(I `),I,w1),(RI `)) is Element of the carrier of X
((X,(I `),I,w1) \ (RI `)) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . (((X,(I `),I,w1) \ (RI `)),(X,(0. X),RI,w1)) is Element of the carrier of X
(X,(I `),I,w1) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . ((X,(I `),I,w1),(X,(0. X),RI,w1)) is Element of the carrier of X
((X,(I `),I,w1) \ (X,(0. X),RI,w1)) \ (RI `) is Element of the carrier of X
the InternalDiff of X . (((X,(I `),I,w1) \ (X,(0. X),RI,w1)),(RI `)) is Element of the carrier of X
(X,(0. X),I,w1) \ I is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,w1),I) is Element of the carrier of X
((X,(0. X),I,w1) \ I) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,w1) \ I),(X,(0. X),RI,w1)) is Element of the carrier of X
(((X,(0. X),I,w1) \ I) \ (X,(0. X),RI,w1)) \ (RI `) is Element of the carrier of X
the InternalDiff of X . ((((X,(0. X),I,w1) \ I) \ (X,(0. X),RI,w1)),(RI `)) is Element of the carrier of X
(X,(0. X),I,(w1 + 1)) is Element of the carrier of X
(X,(0. X),I,(w1 + 1)) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,(w1 + 1)),(X,(0. X),RI,w1)) is Element of the carrier of X
((X,(0. X),I,(w1 + 1)) \ (X,(0. X),RI,w1)) \ (RI `) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,(w1 + 1)) \ (X,(0. X),RI,w1)),(RI `)) is Element of the carrier of X
(X,(0. X),I,(w1 + 1)) \ (RI `) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,(w1 + 1)),(RI `)) is Element of the carrier of X
((X,(0. X),I,(w1 + 1)) \ (RI `)) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),I,(w1 + 1)) \ (RI `)),(X,(0. X),RI,w1)) is Element of the carrier of X
(RI `) ` is Element of the carrier of X
(0. X) \ (RI `) is Element of the carrier of X
the InternalDiff of X . ((0. X),(RI `)) is Element of the carrier of X
(X,((RI `) `),I,(w1 + 1)) is Element of the carrier of X
(X,((RI `) `),I,(w1 + 1)) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . ((X,((RI `) `),I,(w1 + 1)),(X,(0. X),RI,w1)) is Element of the carrier of X
((RI `) `) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . (((RI `) `),(X,(0. X),RI,w1)) is Element of the carrier of X
(X,(((RI `) `) \ (X,(0. X),RI,w1)),I,(w1 + 1)) is Element of the carrier of X
(X,(0. X),RI,w1) ` is Element of the carrier of X
(0. X) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),RI,w1)) is Element of the carrier of X
((X,(0. X),RI,w1) `) \ (RI `) is Element of the carrier of X
the InternalDiff of X . (((X,(0. X),RI,w1) `),(RI `)) is Element of the carrier of X
(X,(((X,(0. X),RI,w1) `) \ (RI `)),I,(w1 + 1)) is Element of the carrier of X
(X,(0. X),RI,w1) \ RI is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),RI,w1),RI) is Element of the carrier of X
((X,(0. X),RI,w1) \ RI) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),RI,w1) \ RI) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),RI,w1) \ RI)) is Element of the carrier of X
(X,(((X,(0. X),RI,w1) \ RI) `),I,(w1 + 1)) is Element of the carrier of X
(X,(0. X),RI,(w1 + 1)) is Element of the carrier of X
(X,(0. X),RI,(w1 + 1)) ` is Element of the carrier of X
(0. X) \ (X,(0. X),RI,(w1 + 1)) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),RI,(w1 + 1))) is Element of the carrier of X
(X,((X,(0. X),RI,(w1 + 1)) `),I,(w1 + 1)) is Element of the carrier of X
(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
(X,(0. X),(I \ RI),0) is Element of the carrier of X
(X,(0. X),I,0) is Element of the carrier of X
(X,(0. X),I,0) \ (0. X) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,0),(0. X)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(I \ RI),w1) is Element of the carrier of X
(X,(0. X),I,w1) is Element of the carrier of X
(X,(0. X),RI,w1) is Element of the carrier of X
(X,(0. X),I,w1) \ (X,(0. X),RI,w1) is Element of the carrier of X
the InternalDiff of X . ((X,(0. X),I,w1),(X,(0. X),RI,w1)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
IT is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,IT,w1) is Element of the carrier of X
(X,RI,IT,w1) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,IT,x1) is Element of the carrier of X
(X,RI,IT,x1) is Element of the carrier of X
(X,I,IT,x1) is Element of the carrier of X
(X,RI,IT,x1) is Element of the carrier of X
(X,I,IT,x1) \ IT is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((X,I,IT,x1),IT) is Element of the carrier of X
(X,RI,IT,x1) \ IT is Element of the carrier of X
the InternalDiff of X . ((X,RI,IT,x1),IT) is Element of the carrier of X
(X,I,IT,(x1 + 1)) is Element of the carrier of X
(X,I,IT,0) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,IT,x1) is Element of the carrier of X
(X,RI,IT,x1) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
IT is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,IT,RI,w1) is Element of the carrier of X
(X,IT,I,w1) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,IT,I,x1) is Element of the carrier of X
(X,IT,I,x1) \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((X,IT,I,x1),RI) is Element of the carrier of X
(X,IT,I,x1) \ I is Element of the carrier of X
the InternalDiff of X . ((X,IT,I,x1),I) is Element of the carrier of X
(X,IT,I,(x1 + 1)) is Element of the carrier of X
((X,IT,I,x1) \ RI) \ (X,IT,I,(x1 + 1)) is Element of the carrier of X
the InternalDiff of X . (((X,IT,I,x1) \ RI),(X,IT,I,(x1 + 1))) is Element of the carrier of X
0. X is V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,IT,RI,x1) is Element of the carrier of X
(X,IT,I,x1) is Element of the carrier of X
(X,IT,RI,x1) is Element of the carrier of X
(X,IT,RI,x1) \ RI is Element of the carrier of X
the InternalDiff of X . ((X,IT,RI,x1),RI) is Element of the carrier of X
(X,IT,RI,(x1 + 1)) is Element of the carrier of X
(X,IT,RI,(x1 + 1)) \ ((X,IT,I,x1) \ RI) is Element of the carrier of X
the InternalDiff of X . ((X,IT,RI,(x1 + 1)),((X,IT,I,x1) \ RI)) is Element of the carrier of X
(X,IT,RI,(x1 + 1)) \ (X,IT,I,(x1 + 1)) is Element of the carrier of X
the InternalDiff of X . ((X,IT,RI,(x1 + 1)),(X,IT,I,(x1 + 1))) is Element of the carrier of X
IT \ IT is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (IT,IT) is Element of the carrier of X
0. X is V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
(X,IT,RI,0) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,IT,RI,x1) is Element of the carrier of X
(X,IT,I,x1) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
IT is Element of the carrier of X
I \ IT is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (I,IT) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,w1) is Element of the carrier of X
(X,IT,RI,w1) is Element of the carrier of X
(X,I,RI,w1) \ (X,IT,RI,w1) is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,w1),(X,IT,RI,w1)) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,x1) is Element of the carrier of X
(X,IT,RI,x1) is Element of the carrier of X
(X,I,RI,x1) \ (X,IT,RI,x1) is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,x1),(X,IT,RI,x1)) is Element of the carrier of X
(X,I,RI,x1) is Element of the carrier of X
(X,IT,RI,x1) is Element of the carrier of X
(X,I,RI,x1) \ (X,IT,RI,x1) is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,x1),(X,IT,RI,x1)) is Element of the carrier of X
((X,I,RI,x1) \ (X,IT,RI,x1)) \ (I \ IT) is Element of the carrier of X
the InternalDiff of X . (((X,I,RI,x1) \ (X,IT,RI,x1)),(I \ IT)) is Element of the carrier of X
0. X is V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
(X,I,RI,x1) \ (I \ IT) is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,x1),(I \ IT)) is Element of the carrier of X
((X,I,RI,x1) \ (I \ IT)) \ (X,IT,RI,x1) is Element of the carrier of X
the InternalDiff of X . (((X,I,RI,x1) \ (I \ IT)),(X,IT,RI,x1)) is Element of the carrier of X
((X,I,RI,x1) \ (I \ IT)) \ RI is Element of the carrier of X
the InternalDiff of X . (((X,I,RI,x1) \ (I \ IT)),RI) is Element of the carrier of X
(X,IT,RI,x1) \ RI is Element of the carrier of X
the InternalDiff of X . ((X,IT,RI,x1),RI) is Element of the carrier of X
(((X,I,RI,x1) \ (I \ IT)) \ RI) \ ((X,IT,RI,x1) \ RI) is Element of the carrier of X
the InternalDiff of X . ((((X,I,RI,x1) \ (I \ IT)) \ RI),((X,IT,RI,x1) \ RI)) is Element of the carrier of X
(X,I,RI,x1) \ RI is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,x1),RI) is Element of the carrier of X
((X,I,RI,x1) \ RI) \ (I \ IT) is Element of the carrier of X
the InternalDiff of X . (((X,I,RI,x1) \ RI),(I \ IT)) is Element of the carrier of X
(((X,I,RI,x1) \ RI) \ (I \ IT)) \ ((X,IT,RI,x1) \ RI) is Element of the carrier of X
the InternalDiff of X . ((((X,I,RI,x1) \ RI) \ (I \ IT)),((X,IT,RI,x1) \ RI)) is Element of the carrier of X
(X,I,RI,(x1 + 1)) is Element of the carrier of X
(X,I,RI,(x1 + 1)) \ (I \ IT) is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,(x1 + 1)),(I \ IT)) is Element of the carrier of X
((X,I,RI,(x1 + 1)) \ (I \ IT)) \ ((X,IT,RI,x1) \ RI) is Element of the carrier of X
the InternalDiff of X . (((X,I,RI,(x1 + 1)) \ (I \ IT)),((X,IT,RI,x1) \ RI)) is Element of the carrier of X
(X,IT,RI,(x1 + 1)) is Element of the carrier of X
((X,I,RI,(x1 + 1)) \ (I \ IT)) \ (X,IT,RI,(x1 + 1)) is Element of the carrier of X
the InternalDiff of X . (((X,I,RI,(x1 + 1)) \ (I \ IT)),(X,IT,RI,(x1 + 1))) is Element of the carrier of X
(X,I,RI,(x1 + 1)) \ (X,IT,RI,(x1 + 1)) is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,(x1 + 1)),(X,IT,RI,(x1 + 1))) is Element of the carrier of X
((X,I,RI,(x1 + 1)) \ (X,IT,RI,(x1 + 1))) \ (I \ IT) is Element of the carrier of X
the InternalDiff of X . (((X,I,RI,(x1 + 1)) \ (X,IT,RI,(x1 + 1))),(I \ IT)) is Element of the carrier of X
(I \ IT) \ (I \ IT) is Element of the carrier of X
the InternalDiff of X . ((I \ IT),(I \ IT)) is Element of the carrier of X
0. X is V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
(X,I,RI,0) is Element of the carrier of X
(X,I,RI,0) \ IT is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,0),IT) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,RI,x1) is Element of the carrier of X
(X,IT,RI,x1) is Element of the carrier of X
(X,I,RI,x1) \ (X,IT,RI,x1) is Element of the carrier of X
the InternalDiff of X . ((X,I,RI,x1),(X,IT,RI,x1)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
I \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (I,RI) is Element of the carrier of X
RI \ I is Element of the carrier of X
the InternalDiff of X . (RI,I) is Element of the carrier of X
IT is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(I \ RI),IT) is Element of the carrier of X
(X,(X,I,(I \ RI),IT),(RI \ I),IT) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(I \ RI),x1) is Element of the carrier of X
(X,(X,I,(I \ RI),x1),(RI \ I),x1) is Element of the carrier of X
(X,I,(I \ RI),w1) is Element of the carrier of X
(X,(X,I,(I \ RI),w1),(RI \ I),w1) is Element of the carrier of X
(X,(X,I,(I \ RI),w1),(RI \ I),w1) \ I is Element of the carrier of X
the InternalDiff of X . ((X,(X,I,(I \ RI),w1),(RI \ I),w1),I) is Element of the carrier of X
0. X is V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
(X,I,(I \ RI),w1) \ I is Element of the carrier of X
the InternalDiff of X . ((X,I,(I \ RI),w1),I) is Element of the carrier of X
(X,((X,I,(I \ RI),w1) \ I),(RI \ I),w1) is Element of the carrier of X
(X,((X,I,(I \ RI),w1) \ I),(RI \ I),w1) \ (RI \ I) is Element of the carrier of X
the InternalDiff of X . ((X,((X,I,(I \ RI),w1) \ I),(RI \ I),w1),(RI \ I)) is Element of the carrier of X
(RI \ I) ` is Element of the carrier of X
(0. X) \ (RI \ I) is Element of the carrier of X
the InternalDiff of X . ((0. X),(RI \ I)) is Element of the carrier of X
(X,((X,I,(I \ RI),w1) \ I),(RI \ I),(w1 + 1)) is Element of the carrier of X
(X,((X,I,(I \ RI),w1) \ I),(RI \ I),(w1 + 1)) \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . ((X,((X,I,(I \ RI),w1) \ I),(RI \ I),(w1 + 1)),(I \ RI)) is Element of the carrier of X
((RI \ I) `) \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . (((RI \ I) `),(I \ RI)) is Element of the carrier of X
((X,I,(I \ RI),w1) \ I) \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . (((X,I,(I \ RI),w1) \ I),(I \ RI)) is Element of the carrier of X
(X,(((X,I,(I \ RI),w1) \ I) \ (I \ RI)),(RI \ I),(w1 + 1)) is Element of the carrier of X
(X,I,(I \ RI),w1) \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . ((X,I,(I \ RI),w1),(I \ RI)) is Element of the carrier of X
((X,I,(I \ RI),w1) \ (I \ RI)) \ I is Element of the carrier of X
the InternalDiff of X . (((X,I,(I \ RI),w1) \ (I \ RI)),I) is Element of the carrier of X
(X,(((X,I,(I \ RI),w1) \ (I \ RI)) \ I),(RI \ I),(w1 + 1)) is Element of the carrier of X
(X,I,(I \ RI),(w1 + 1)) is Element of the carrier of X
(X,I,(I \ RI),(w1 + 1)) \ I is Element of the carrier of X
the InternalDiff of X . ((X,I,(I \ RI),(w1 + 1)),I) is Element of the carrier of X
(X,((X,I,(I \ RI),(w1 + 1)) \ I),(RI \ I),(w1 + 1)) is Element of the carrier of X
RI \ RI is Element of the carrier of X
the InternalDiff of X . (RI,RI) is Element of the carrier of X
(RI \ RI) \ (RI \ I) is Element of the carrier of X
the InternalDiff of X . ((RI \ RI),(RI \ I)) is Element of the carrier of X
((RI \ RI) \ (RI \ I)) \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . (((RI \ RI) \ (RI \ I)),(I \ RI)) is Element of the carrier of X
(X,(X,I,(I \ RI),(w1 + 1)),(RI \ I),(w1 + 1)) is Element of the carrier of X
(X,(X,I,(I \ RI),(w1 + 1)),(RI \ I),(w1 + 1)) \ I is Element of the carrier of X
the InternalDiff of X . ((X,(X,I,(I \ RI),(w1 + 1)),(RI \ I),(w1 + 1)),I) is Element of the carrier of X
I \ I is Element of the carrier of X
the InternalDiff of X . (I,I) is Element of the carrier of X
0. X is V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
(X,I,(RI \ I),0) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,I,(I \ RI),w1) is Element of the carrier of X
(X,(X,I,(I \ RI),w1),(RI \ I),w1) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
RI \ I is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (RI,I) is Element of the carrier of X
0. X is V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
RI is Element of the carrier of X
RI \ I is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (RI,I) is Element of the carrier of X
0. X is V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
0. X is V44(X) Element of the carrier of X
the carrier of X is non empty set
the ZeroF of X is Element of the carrier of X
(0. X) ` is Element of the carrier of X
(0. X) \ (0. X) is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),(0. X)) is Element of the carrier of X
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 V44(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
0. X is V44(X) Element of the carrier of X
the carrier of X is non empty set
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
I \ (0. X) is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (I,(0. X)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
0. X is V44(X) Element of the carrier of X
the carrier of X is non empty set
the ZeroF of X is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
I ` is Element of the carrier of X
0. X is V44(X) atom (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
(0. X) \ I is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),I) is Element of the carrier of X
RI is Element of the carrier of X
I \ RI is Element of the carrier of X
the InternalDiff of X . (I,RI) is Element of the carrier of X
RI ` is Element of the carrier of X
(0. X) \ RI is Element of the carrier of X
the InternalDiff of X . ((0. X),RI) is Element of the carrier of X
(RI `) \ (I `) is Element of the carrier of X
the InternalDiff of X . ((RI `),(I `)) is Element of the carrier of X
RI \ I is Element of the carrier of X
the InternalDiff of X . (RI,I) is Element of the carrier of X
RI \ (RI \ I) is Element of the carrier of X
the InternalDiff of X . (RI,(RI \ I)) is Element of the carrier of X
(RI \ (RI \ I)) \ I is Element of the carrier of X
the InternalDiff of X . ((RI \ (RI \ I)),I) is Element of the carrier of X
(I \ RI) \ ((RI `) \ (I `)) is Element of the carrier of X
the InternalDiff of X . ((I \ RI),((RI `) \ (I `))) is Element of the carrier of X
(RI \ (RI \ I)) \ RI is Element of the carrier of X
the InternalDiff of X . ((RI \ (RI \ I)),RI) is Element of the carrier of X
((RI \ (RI \ I)) \ RI) \ ((RI `) \ (I `)) is Element of the carrier of X
the InternalDiff of X . (((RI \ (RI \ I)) \ RI),((RI `) \ (I `))) is Element of the carrier of X
RI \ RI is Element of the carrier of X
the InternalDiff of X . (RI,RI) is Element of the carrier of X
(RI \ RI) \ (RI \ I) is Element of the carrier of X
the InternalDiff of X . ((RI \ RI),(RI \ I)) is Element of the carrier of X
((RI \ RI) \ (RI \ I)) \ ((RI `) \ (I `)) is Element of the carrier of X
the InternalDiff of X . (((RI \ RI) \ (RI \ I)),((RI `) \ (I `))) is Element of the carrier of X
(RI \ I) ` is Element of the carrier of X
(0. X) \ (RI \ I) is Element of the carrier of X
the InternalDiff of X . ((0. X),(RI \ I)) is Element of the carrier of X
((RI \ I) `) \ ((RI `) \ (I `)) is Element of the carrier of X
the InternalDiff of X . (((RI \ I) `),((RI `) \ (I `))) is Element of the carrier of X
((RI \ I) `) \ ((RI \ I) `) is Element of the carrier of X
the InternalDiff of X . (((RI \ I) `),((RI \ I) `)) is Element of the carrier of X
((RI `) \ (I `)) \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . (((RI `) \ (I `)),(I \ RI)) is Element of the carrier of X
RI is Element of the carrier of X
RI \ I is Element of the carrier of X
the InternalDiff of X . (RI,I) is Element of the carrier of X
I \ RI is Element of the carrier of X
the InternalDiff of X . (I,RI) is Element of the carrier of X
RI ` is Element of the carrier of X
(0. X) \ RI is Element of the carrier of X
the InternalDiff of X . ((0. X),RI) is Element of the carrier of X
(RI `) \ (I `) is Element of the carrier of X
the InternalDiff of X . ((RI `),(I `)) is Element of the carrier of X
(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
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
I ` is Element of the carrier of X
0. X is V44(X) atom (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
(0. X) \ I is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),I) is Element of the carrier of X
RI is Element of the carrier of X
RI ` is Element of the carrier of X
(0. X) \ RI is Element of the carrier of X
the InternalDiff of X . ((0. X),RI) is Element of the carrier of X
RI \ I is Element of the carrier of X
the InternalDiff of X . (RI,I) is Element of the carrier of X
(RI \ I) ` is Element of the carrier of X
(0. X) \ (RI \ I) is Element of the carrier of X
the InternalDiff of X . ((0. X),(RI \ I)) is Element of the carrier of X
(RI `) \ (I `) is Element of the carrier of X
the InternalDiff of X . ((RI `),(I `)) is Element of the carrier of X
RI is Element of the carrier of X
RI \ (I `) is Element of the carrier of X
the InternalDiff of X . (RI,(I `)) is Element of the carrier of X
(RI \ (I `)) ` is Element of the carrier of X
(0. X) \ (RI \ (I `)) is Element of the carrier of X
the InternalDiff of X . ((0. X),(RI \ (I `))) is Element of the carrier of X
RI ` is Element of the carrier of X
(0. X) \ RI is Element of the carrier of X
the InternalDiff of X . ((0. X),RI) is Element of the carrier of X
(I `) ` is Element of the carrier of X
(0. X) \ (I `) is Element of the carrier of X
the InternalDiff of X . ((0. X),(I `)) is Element of the carrier of X
(RI `) \ ((I `) `) is Element of the carrier of X
the InternalDiff of X . ((RI `),((I `) `)) is Element of the carrier of X
((RI `) \ ((I `) `)) ` is Element of the carrier of X
(0. X) \ ((RI `) \ ((I `) `)) is Element of the carrier of X
the InternalDiff of X . ((0. X),((RI `) \ ((I `) `))) is Element of the carrier of X
(RI `) ` is Element of the carrier of X
(0. X) \ (RI `) is Element of the carrier of X
the InternalDiff of X . ((0. X),(RI `)) is Element of the carrier of X
((I `) `) ` is Element of the carrier of X
(0. X) \ ((I `) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((I `) `)) is Element of the carrier of X
((RI `) `) \ (((I `) `) `) is Element of the carrier of X
the InternalDiff of X . (((RI `) `),(((I `) `) `)) is Element of the carrier of X
((RI `) `) \ (I `) is Element of the carrier of X
the InternalDiff of X . (((RI `) `),(I `)) is Element of the carrier of X
(RI `) \ I is Element of the carrier of X
the InternalDiff of X . ((RI `),I) is Element of the carrier of X
((RI `) \ I) ` is Element of the carrier of X
(0. X) \ ((RI `) \ I) is Element of the carrier of X
the InternalDiff of X . ((0. X),((RI `) \ I)) is Element of the carrier of X
(I `) \ RI is Element of the carrier of X
the InternalDiff of X . ((I `),RI) is Element of the carrier of X
((I `) \ RI) ` is Element of the carrier of X
(0. X) \ ((I `) \ RI) is Element of the carrier of X
the InternalDiff of X . ((0. X),((I `) \ RI)) is Element of the carrier of X
RI \ RI is Element of the carrier of X
the InternalDiff of X . (RI,RI) is Element of the carrier of X
(RI \ RI) \ ((I `) \ RI) is Element of the carrier of X
the InternalDiff of X . ((RI \ RI),((I `) \ RI)) is Element of the carrier of X
((I `) `) \ I is Element of the carrier of X
the InternalDiff of X . (((I `) `),I) is Element of the carrier of X
((RI `) \ I) \ (((I `) `) \ I) is Element of the carrier of X
the InternalDiff of X . (((RI `) \ I),(((I `) `) \ I)) is Element of the carrier of X
((RI `) \ I) \ (0. X) is Element of the carrier of X
the InternalDiff of X . (((RI `) \ I),(0. X)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
I ` is Element of the carrier of X
0. X is V44(X) atom (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
(0. X) \ I is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),I) is Element of the carrier of X
RI is Element of the carrier of X
RI ` is Element of the carrier of X
(0. X) \ RI is Element of the carrier of X
the InternalDiff of X . ((0. X),RI) is Element of the carrier of X
(RI `) \ (I `) is Element of the carrier of X
the InternalDiff of X . ((RI `),(I `)) is Element of the carrier of X
IT is Element of the carrier of X
I \ IT is Element of the carrier of X
the InternalDiff of X . (I,IT) is Element of the carrier of X
RI \ IT is Element of the carrier of X
the InternalDiff of X . (RI,IT) is Element of the carrier of X
(I \ IT) \ (RI \ IT) is Element of the carrier of X
the InternalDiff of X . ((I \ IT),(RI \ IT)) is Element of the carrier of X
((I \ IT) \ (RI \ IT)) ` is Element of the carrier of X
(0. X) \ ((I \ IT) \ (RI \ IT)) is Element of the carrier of X
the InternalDiff of X . ((0. X),((I \ IT) \ (RI \ IT))) is Element of the carrier of X
(((I \ IT) \ (RI \ IT)) `) ` is Element of the carrier of X
(0. X) \ (((I \ IT) \ (RI \ IT)) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),(((I \ IT) \ (RI \ IT)) `)) is Element of the carrier of X
I \ RI is Element of the carrier of X
the InternalDiff of X . (I,RI) is Element of the carrier of X
(RI `) \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . ((RI `),(I \ RI)) is Element of the carrier of X
((RI `) \ (I \ RI)) \ (I `) is Element of the carrier of X
the InternalDiff of X . (((RI `) \ (I \ RI)),(I `)) is Element of the carrier of X
(I \ IT) ` is Element of the carrier of X
(0. X) \ (I \ IT) is Element of the carrier of X
the InternalDiff of X . ((0. X),(I \ IT)) is Element of the carrier of X
(RI \ IT) ` is Element of the carrier of X
(0. X) \ (RI \ IT) is Element of the carrier of X
the InternalDiff of X . ((0. X),(RI \ IT)) is Element of the carrier of X
((I \ IT) `) \ ((RI \ IT) `) is Element of the carrier of X
the InternalDiff of X . (((I \ IT) `),((RI \ IT) `)) is Element of the carrier of X
(((I \ IT) `) \ ((RI \ IT) `)) ` is Element of the carrier of X
(0. X) \ (((I \ IT) `) \ ((RI \ IT) `)) is Element of the carrier of X
the InternalDiff of X . ((0. X),(((I \ IT) `) \ ((RI \ IT) `))) is Element of the carrier of X
IT ` is Element of the carrier of X
(0. X) \ IT is Element of the carrier of X
the InternalDiff of X . ((0. X),IT) is Element of the carrier of X
(I `) \ (IT `) is Element of the carrier of X
the InternalDiff of X . ((I `),(IT `)) is Element of the carrier of X
((I `) \ (IT `)) \ ((RI \ IT) `) is Element of the carrier of X
the InternalDiff of X . (((I `) \ (IT `)),((RI \ IT) `)) is Element of the carrier of X
(((I `) \ (IT `)) \ ((RI \ IT) `)) ` is Element of the carrier of X
(0. X) \ (((I `) \ (IT `)) \ ((RI \ IT) `)) is Element of the carrier of X
the InternalDiff of X . ((0. X),(((I `) \ (IT `)) \ ((RI \ IT) `))) is Element of the carrier of X
((RI `) \ (I \ RI)) \ (IT `) is Element of the carrier of X
the InternalDiff of X . (((RI `) \ (I \ RI)),(IT `)) is Element of the carrier of X
(((RI `) \ (I \ RI)) \ (IT `)) \ ((RI \ IT) `) is Element of the carrier of X
the InternalDiff of X . ((((RI `) \ (I \ RI)) \ (IT `)),((RI \ IT) `)) is Element of the carrier of X
((((RI `) \ (I \ RI)) \ (IT `)) \ ((RI \ IT) `)) ` is Element of the carrier of X
(0. X) \ ((((RI `) \ (I \ RI)) \ (IT `)) \ ((RI \ IT) `)) is Element of the carrier of X
the InternalDiff of X . ((0. X),((((RI `) \ (I \ RI)) \ (IT `)) \ ((RI \ IT) `))) is Element of the carrier of X
(RI `) \ (IT `) is Element of the carrier of X
the InternalDiff of X . ((RI `),(IT `)) is Element of the carrier of X
((RI `) \ (IT `)) \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . (((RI `) \ (IT `)),(I \ RI)) is Element of the carrier of X
(((RI `) \ (IT `)) \ (I \ RI)) \ ((RI \ IT) `) is Element of the carrier of X
the InternalDiff of X . ((((RI `) \ (IT `)) \ (I \ RI)),((RI \ IT) `)) is Element of the carrier of X
((((RI `) \ (IT `)) \ (I \ RI)) \ ((RI \ IT) `)) ` is Element of the carrier of X
(0. X) \ ((((RI `) \ (IT `)) \ (I \ RI)) \ ((RI \ IT) `)) is Element of the carrier of X
the InternalDiff of X . ((0. X),((((RI `) \ (IT `)) \ (I \ RI)) \ ((RI \ IT) `))) is Element of the carrier of X
((RI \ IT) `) \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . (((RI \ IT) `),(I \ RI)) is Element of the carrier of X
(((RI \ IT) `) \ (I \ RI)) \ ((RI \ IT) `) is Element of the carrier of X
the InternalDiff of X . ((((RI \ IT) `) \ (I \ RI)),((RI \ IT) `)) is Element of the carrier of X
((((RI \ IT) `) \ (I \ RI)) \ ((RI \ IT) `)) ` is Element of the carrier of X
(0. X) \ ((((RI \ IT) `) \ (I \ RI)) \ ((RI \ IT) `)) is Element of the carrier of X
the InternalDiff of X . ((0. X),((((RI \ IT) `) \ (I \ RI)) \ ((RI \ IT) `))) is Element of the carrier of X
((RI \ IT) `) \ ((RI \ IT) `) is Element of the carrier of X
the InternalDiff of X . (((RI \ IT) `),((RI \ IT) `)) is Element of the carrier of X
(((RI \ IT) `) \ ((RI \ IT) `)) \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . ((((RI \ IT) `) \ ((RI \ IT) `)),(I \ RI)) is Element of the carrier of X
((((RI \ IT) `) \ ((RI \ IT) `)) \ (I \ RI)) ` is Element of the carrier of X
(0. X) \ ((((RI \ IT) `) \ ((RI \ IT) `)) \ (I \ RI)) is Element of the carrier of X
the InternalDiff of X . ((0. X),((((RI \ IT) `) \ ((RI \ IT) `)) \ (I \ RI))) is Element of the carrier of X
(I \ RI) ` is Element of the carrier of X
(0. X) \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . ((0. X),(I \ RI)) is Element of the carrier of X
((I \ RI) `) ` is Element of the carrier of X
(0. X) \ ((I \ RI) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((I \ RI) `)) is Element of the carrier of X
(I `) \ (RI `) is Element of the carrier of X
the InternalDiff of X . ((I `),(RI `)) is Element of the carrier of X
((I `) \ (RI `)) ` is Element of the carrier of X
(0. X) \ ((I `) \ (RI `)) is Element of the carrier of X
the InternalDiff of X . ((0. X),((I `) \ (RI `))) is Element of the carrier of X
(RI `) ` is Element of the carrier of X
(0. X) \ (RI `) is Element of the carrier of X
the InternalDiff of X . ((0. X),(RI `)) is Element of the carrier of X
((RI `) `) \ I is Element of the carrier of X
the InternalDiff of X . (((RI `) `),I) is Element of the carrier of X
(((RI `) `) \ I) ` is Element of the carrier of X
(0. X) \ (((RI `) `) \ I) is Element of the carrier of X
the InternalDiff of X . ((0. X),(((RI `) `) \ I)) is Element of the carrier of X
((RI `) `) ` is Element of the carrier of X
(0. X) \ ((RI `) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((RI `) `)) is Element of the carrier of X
(((RI `) `) `) \ (I `) is Element of the carrier of X
the InternalDiff of X . ((((RI `) `) `),(I `)) is Element of the carrier of X
RI is Element of the carrier of X
RI \ (I `) is Element of the carrier of X
the InternalDiff of X . (RI,(I `)) is Element of the carrier of X
RI ` is Element of the carrier of X
(0. X) \ RI is Element of the carrier of X
the InternalDiff of X . ((0. X),RI) is Element of the carrier of X
(RI `) \ (I `) is Element of the carrier of X
the InternalDiff of X . ((RI `),(I `)) is Element of the carrier of X
(RI `) \ RI is Element of the carrier of X
the InternalDiff of X . ((RI `),RI) is Element of the carrier of X
((RI `) \ (I `)) \ ((RI `) \ RI) is Element of the carrier of X
the InternalDiff of X . (((RI `) \ (I `)),((RI `) \ RI)) is Element of the carrier of X
I \ (0. X) is Element of the carrier of X
the InternalDiff of X . (I,(0. X)) is Element of the carrier of X
RI \ (0. X) is Element of the carrier of X
the InternalDiff of X . (RI,(0. X)) is Element of the carrier of X
(I \ (0. X)) \ (RI \ (0. X)) is Element of the carrier of X
the InternalDiff of X . ((I \ (0. X)),(RI \ (0. X))) is Element of the carrier of X
((I \ (0. X)) \ (RI \ (0. X))) ` is Element of the carrier of X
(0. X) \ ((I \ (0. X)) \ (RI \ (0. X))) is Element of the carrier of X
the InternalDiff of X . ((0. X),((I \ (0. X)) \ (RI \ (0. X)))) is Element of the carrier of X
(((I \ (0. X)) \ (RI \ (0. X))) `) ` is Element of the carrier of X
(0. X) \ (((I \ (0. X)) \ (RI \ (0. X))) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),(((I \ (0. X)) \ (RI \ (0. X))) `)) is Element of the carrier of X
((((I \ (0. X)) \ (RI \ (0. X))) `) `) \ ((RI `) \ RI) is Element of the carrier of X
the InternalDiff of X . (((((I \ (0. X)) \ (RI \ (0. X))) `) `),((RI `) \ RI)) is Element of the carrier of X
((RI `) \ RI) ` is Element of the carrier of X
(0. X) \ ((RI `) \ RI) is Element of the carrier of X
the InternalDiff of X . ((0. X),((RI `) \ RI)) is Element of the carrier of X
(((RI `) \ RI) `) \ (((I \ (0. X)) \ (RI \ (0. X))) `) is Element of the carrier of X
the InternalDiff of X . ((((RI `) \ RI) `),(((I \ (0. X)) \ (RI \ (0. X))) `)) is Element of the carrier of X
I \ (RI \ (0. X)) is Element of the carrier of X
the InternalDiff of X . (I,(RI \ (0. X))) is Element of the carrier of X
(I \ (RI \ (0. X))) ` is Element of the carrier of X
(0. X) \ (I \ (RI \ (0. X))) is Element of the carrier of X
the InternalDiff of X . ((0. X),(I \ (RI \ (0. X)))) is Element of the carrier of X
(((RI `) \ RI) `) \ ((I \ (RI \ (0. X))) `) is Element of the carrier of X
the InternalDiff of X . ((((RI `) \ RI) `),((I \ (RI \ (0. X))) `)) is Element of the carrier of X
I \ RI is Element of the carrier of X
the InternalDiff of X . (I,RI) is Element of the carrier of X
(I \ RI) ` is Element of the carrier of X
(0. X) \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . ((0. X),(I \ RI)) is Element of the carrier of X
(((RI `) \ RI) `) \ ((I \ RI) `) is Element of the carrier of X
the InternalDiff of X . ((((RI `) \ RI) `),((I \ RI) `)) is Element of the carrier of X
(RI `) ` is Element of the carrier of X
(0. X) \ (RI `) is Element of the carrier of X
the InternalDiff of X . ((0. X),(RI `)) is Element of the carrier of X
((RI `) `) \ (RI `) is Element of the carrier of X
the InternalDiff of X . (((RI `) `),(RI `)) is Element of the carrier of X
(((RI `) `) \ (RI `)) \ ((I \ RI) `) is Element of the carrier of X
the InternalDiff of X . ((((RI `) `) \ (RI `)),((I \ RI) `)) is Element of the carrier of X
(I `) \ (RI `) is Element of the carrier of X
the InternalDiff of X . ((I `),(RI `)) is Element of the carrier of X
(((RI `) `) \ (RI `)) \ ((I `) \ (RI `)) is Element of the carrier of X
the InternalDiff of X . ((((RI `) `) \ (RI `)),((I `) \ (RI `))) is Element of the carrier of X
((RI `) `) \ (I `) is Element of the carrier of X
the InternalDiff of X . (((RI `) `),(I `)) is Element of the carrier of X
(((RI `) `) \ (I `)) ` is Element of the carrier of X
(0. X) \ (((RI `) `) \ (I `)) is Element of the carrier of X
the InternalDiff of X . ((0. X),(((RI `) `) \ (I `))) is Element of the carrier of X
((RI `) `) ` is Element of the carrier of X
(0. X) \ ((RI `) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((RI `) `)) is Element of the carrier of X
(I `) ` is Element of the carrier of X
(0. X) \ (I `) is Element of the carrier of X
the InternalDiff of X . ((0. X),(I `)) is Element of the carrier of X
(((RI `) `) `) \ ((I `) `) is Element of the carrier of X
the InternalDiff of X . ((((RI `) `) `),((I `) `)) is Element of the carrier of X
(RI `) \ ((I `) `) is Element of the carrier of X
the InternalDiff of X . ((RI `),((I `) `)) is Element of the carrier of X
((I `) `) ` is Element of the carrier of X
(0. X) \ ((I `) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((I `) `)) is Element of the carrier of X
(((I `) `) `) \ RI is Element of the carrier of X
the InternalDiff of X . ((((I `) `) `),RI) is Element of the carrier of X
(I `) \ RI is Element of the carrier of X
the InternalDiff of X . ((I `),RI) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
0. X is V44(X) atom (X) Element of the carrier of X
the carrier of X is non empty set
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
RI is Element of the carrier of X
RI \ I is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (RI,I) is Element of the carrier of X
I \ RI is Element of the carrier of X
the InternalDiff of X . (I,RI) is Element of the carrier of X
(I \ RI) ` is Element of the carrier of X
(0. X) \ (I \ RI) is Element of the carrier of X
the InternalDiff of X . ((0. X),(I \ RI)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
RI is Element of the carrier of X
RI \ I is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (RI,I) is Element of the carrier of X
0. X is V44(X) atom (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
(RI \ I) ` is Element of the carrier of X
(0. X) \ (RI \ I) is Element of the carrier of X
the InternalDiff of X . ((0. X),(RI \ I)) is Element of the carrier of X
I ` is Element of the carrier of X
(0. X) \ I is Element of the carrier of X
the InternalDiff of X . ((0. X),I) is Element of the carrier of X
RI ` is Element of the carrier of X
(0. X) \ RI is Element of the carrier of X
the InternalDiff of X . ((0. X),RI) is Element of the carrier of X
(RI `) \ (0. X) is Element of the carrier of X
the InternalDiff of X . ((RI `),(0. X)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
I ` is Element of the carrier of X
0. X is V44(X) atom (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
(0. X) \ I is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),I) is Element of the carrier of X
(I `) ` is Element of the carrier of X
(0. X) \ (I `) is Element of the carrier of X
the InternalDiff of X . ((0. X),(I `)) is Element of the carrier of X
I \ ((I `) `) is Element of the carrier of X
the InternalDiff of X . (I,((I `) `)) is Element of the carrier of X
(I \ ((I `) `)) ` is Element of the carrier of X
(0. X) \ (I \ ((I `) `)) is Element of the carrier of X
the InternalDiff of X . ((0. X),(I \ ((I `) `))) is Element of the carrier of X
((I `) `) ` is Element of the carrier of X
(0. X) \ ((I `) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((I `) `)) is Element of the carrier of X
(I `) \ (((I `) `) `) is Element of the carrier of X
the InternalDiff of X . ((I `),(((I `) `) `)) is Element of the carrier of X
(I `) \ (I `) is Element of the carrier of X
the InternalDiff of X . ((I `),(I `)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
I ` is Element of the carrier of X
0. X is V44(X) atom (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
(0. X) \ I is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),I) is Element of the carrier of X
(I `) ` is Element of the carrier of X
(0. X) \ (I `) is Element of the carrier of X
the InternalDiff of X . ((0. X),(I `)) is Element of the carrier of X
((I `) `) \ I is Element of the carrier of X
the InternalDiff of X . (((I `) `),I) is Element of the carrier of X
RI is Element of the carrier of X
RI \ I is Element of the carrier of X
the InternalDiff of X . (RI,I) is Element of the carrier of X
I \ RI is Element of the carrier of X
the InternalDiff of X . (I,RI) is Element of the carrier of X
RI ` is Element of the carrier of X
(0. X) \ RI is Element of the carrier of X
the InternalDiff of X . ((0. X),RI) is Element of the carrier of X
(RI `) \ (I `) is Element of the carrier of X
the InternalDiff of X . ((RI `),(I `)) is Element of the carrier of X
(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
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
I ` is Element of the carrier of X
0. X is V44(X) atom (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
(0. X) \ I is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),I) is Element of the carrier of X
RI is Element of the carrier of X
RI ` is Element of the carrier of X
(0. X) \ RI is Element of the carrier of X
the InternalDiff of X . ((0. X),RI) is Element of the carrier of X
(RI `) \ I is Element of the carrier of X
the InternalDiff of X . ((RI `),I) is Element of the carrier of X
RI is Element of the carrier of X
RI ` is Element of the carrier of X
0. X is V44(X) atom (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
(0. X) \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),RI) is Element of the carrier of X
IT is Element of the carrier of X
IT \ I is Element of the carrier of X
the InternalDiff of X . (IT,I) is Element of the carrier of X
I \ IT is Element of the carrier of X
the InternalDiff of X . (I,IT) is Element of the carrier of X
IT \ (RI `) is Element of the carrier of X
the InternalDiff of X . (IT,(RI `)) is Element of the carrier of X
(IT \ (RI `)) \ IT is Element of the carrier of X
the InternalDiff of X . ((IT \ (RI `)),IT) is Element of the carrier of X
((IT \ (RI `)) \ IT) \ RI is Element of the carrier of X
the InternalDiff of X . (((IT \ (RI `)) \ IT),RI) is Element of the carrier of X
IT \ IT is Element of the carrier of X
the InternalDiff of X . (IT,IT) is Element of the carrier of X
(IT \ IT) \ (RI `) is Element of the carrier of X
the InternalDiff of X . ((IT \ IT),(RI `)) is Element of the carrier of X
((IT \ IT) \ (RI `)) \ RI is Element of the carrier of X
the InternalDiff of X . (((IT \ IT) \ (RI `)),RI) is Element of the carrier of X
(RI `) ` is Element of the carrier of X
(0. X) \ (RI `) is Element of the carrier of X
the InternalDiff of X . ((0. X),(RI `)) is Element of the carrier of X
((RI `) `) \ RI is Element of the carrier of X
the InternalDiff of X . (((RI `) `),RI) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
0. X is V44(X) atom (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
RI is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,RI) is Element of the carrier of X
RI is V21() V22() V23() V27() V74() ext-real non negative V78() set
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,w1) is Element of the carrier of X
IT is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,IT) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,w1) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,x1) is Element of the carrier of X
RI is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,RI) is Element of the carrier of X
IT is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,IT) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
0. X is V44(X) atom (X) Element of the carrier of X
the carrier of X is non empty set
the ZeroF of X is Element of the carrier of X
(X,(0. X),(0. X),1) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
(X,I) is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
0. X is V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I ` is Element of the carrier of X
(0. X) \ I is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),I) is Element of the carrier of X
(X,(0. X),I,1) is Element of the carrier of X
IT is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,IT) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,w1) is Element of the carrier of X
0. X is V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
(X,(0. X),I,1) is Element of the carrier of X
I ` is Element of the carrier of X
(0. X) \ I is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),I) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
RI is Element of the carrier of X
(X,RI) is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
RI ` is Element of the carrier of X
0. X is V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
(0. X) \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),RI) is Element of the carrier of X
(X,(0. X),RI,1) is Element of the carrier of X
IT is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),RI,w1) is Element of the carrier of X
(X,(0. X),RI,IT) is Element of the carrier of X
I is Element of the carrier of X
(X,I) is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
0. X is V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
(X,(0. X),I,1) is Element of the carrier of X
I ` is Element of the carrier of X
(0. X) \ I is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),I) is Element of the carrier of X
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 V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
I ` is Element of the carrier of X
(0. X) \ I is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),I) is Element of the carrier of X
RI is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(I `),RI) is Element of the carrier of X
(X,(0. X),I,RI) is Element of the carrier of X
(X,(0. X),I,RI) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,RI) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,RI)) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Element of the carrier of X
(X,I) is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
I ` is Element of the carrier of X
0. X is V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
(0. X) \ I is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),I) is Element of the carrier of X
(X,(I `)) is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
RI is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),I,RI) is Element of the carrier of X
(X,(0. X),(I `),RI) is Element of the carrier of X
(X,(0. X),I,RI) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,RI) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,RI)) is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(0. X),(I `),w1) is Element of the carrier of X
(X,(0. X),I,w1) is Element of the carrier of X
(X,(0. X),I,w1) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,w1) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,w1)) is Element of the carrier of X
((X,(0. X),I,w1) `) ` is Element of the carrier of X
(0. X) \ ((X,(0. X),I,w1) `) is Element of the carrier of X
the InternalDiff of X . ((0. X),((X,(0. X),I,w1) `)) is Element of the carrier of X
(X,(0. X),(I `),(X,I)) is Element of the carrier of X
(X,(0. X),I,(X,I)) is Element of the carrier of X
(X,(0. X),I,(X,I)) ` is Element of the carrier of X
(0. X) \ (X,(0. X),I,(X,I)) is Element of the carrier of X
the InternalDiff of X . ((0. X),(X,(0. X),I,(X,I))) is Element of the carrier of X
(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
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
[: the carrier of X, the carrier of X:] is non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
id the carrier of X is Relation-like the carrier of X -defined the carrier of X -valued non empty total reflexive symmetric antisymmetric transitive Element of bool [: the carrier of X, the carrier of X:]
I is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive Element of bool [: the carrier of X, the carrier of X:]
RI is Element of the carrier of X
IT is Element of the carrier of X
[RI,IT] is set
{RI,IT} is set
{RI} is set
{{RI,IT},{RI}} is set
w1 is Element of the carrier of X
x1 is Element of the carrier of X
[w1,x1] is set
{w1,x1} is set
{w1} is set
{{w1,x1},{w1}} is set
RI \ w1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (RI,w1) is Element of the carrier of X
IT \ x1 is Element of the carrier of X
the InternalDiff of X . (IT,x1) is Element of the carrier of X
[(RI \ w1),(IT \ x1)] is set
{(RI \ w1),(IT \ x1)} is set
{(RI \ w1)} is set
{{(RI \ w1),(IT \ x1)},{(RI \ w1)}} 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
[: the carrier of X, the carrier of X:] is non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
id the carrier of X is Relation-like the carrier of X -defined the carrier of X -valued non empty total reflexive symmetric antisymmetric transitive Element of bool [: the carrier of X, the carrier of X:]
I is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive Element of bool [: the carrier of X, the carrier of X:]
RI is Element of the carrier of X
IT is Element of the carrier of X
[RI,IT] is set
{RI,IT} is set
{RI} is set
{{RI,IT},{RI}} is set
w1 is Element of the carrier of X
w1 \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (w1,RI) is Element of the carrier of X
w1 \ IT is Element of the carrier of X
the InternalDiff of X . (w1,IT) is Element of the carrier of X
[(w1 \ RI),(w1 \ IT)] is set
{(w1 \ RI),(w1 \ IT)} is set
{(w1 \ RI)} is set
{{(w1 \ RI),(w1 \ IT)},{(w1 \ RI)}} 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
[: the carrier of X, the carrier of X:] is non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
id the carrier of X is Relation-like the carrier of X -defined the carrier of X -valued non empty total reflexive symmetric antisymmetric transitive Element of bool [: the carrier of X, the carrier of X:]
I is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive Element of bool [: the carrier of X, the carrier of X:]
RI is Element of the carrier of X
IT is Element of the carrier of X
[RI,IT] is set
{RI,IT} is set
{RI} is set
{{RI,IT},{RI}} is set
w1 is Element of the carrier of X
RI \ w1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (RI,w1) is Element of the carrier of X
IT \ w1 is Element of the carrier of X
the InternalDiff of X . (IT,w1) is Element of the carrier of X
[(RI \ w1),(IT \ w1)] is set
{(RI \ w1),(IT \ w1)} is set
{(RI \ w1)} is set
{{(RI \ w1),(IT \ w1)},{(RI \ w1)}} 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
[: the carrier of X, the carrier of X:] is non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
I is non empty Ideal of X
RI is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
IT is Element of the carrier of X
w1 is Element of the carrier of X
[IT,w1] is set
{IT,w1} is set
{IT} is set
{{IT,w1},{IT}} is set
IT \ w1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (IT,w1) is Element of the carrier of X
w1 \ IT is Element of the carrier of X
the InternalDiff of X . (w1,IT) is Element of the carrier of X
x1 is Element of the carrier of X
x1 is Element of the carrier of X
x1 \ x1 is Element of the carrier of X
the InternalDiff of X . (x1,x1) is Element of the carrier of X
x1 \ x1 is Element of the carrier of X
the InternalDiff of X . (x1,x1) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is non empty Ideal of X
[: the carrier of X, the carrier of X:] is non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
RI is Relation-like the carrier of X -defined the carrier of X -valued (X,I)
IT is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
w1 is set
[w1,w1] is set
{w1,w1} is set
{w1} is set
{{w1,w1},{w1}} is set
0. X is V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
x1 is Element of the carrier of X
x1 \ x1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (x1,x1) is Element of the carrier of X
field IT is set
dom IT is set
rng IT is set
(dom IT) \/ (rng IT) is set
w1 is set
x1 is set
[w1,x1] is set
{w1,x1} is set
{w1} is set
{{w1,x1},{w1}} is set
x1 is set
[x1,x1] is set
{x1,x1} is set
{x1} is set
{{x1,x1},{x1}} is set
[w1,x1] is set
{w1,x1} is set
{{w1,x1},{w1}} is set
y1 is Element of the carrier of X
y1 is Element of the carrier of X
y1 \ y1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (y1,y1) is Element of the carrier of X
x1 is Element of the carrier of X
x1 \ y1 is Element of the carrier of X
the InternalDiff of X . (x1,y1) is Element of the carrier of X
(y1 \ y1) \ (x1 \ y1) is Element of the carrier of X
the InternalDiff of X . ((y1 \ y1),(x1 \ y1)) is Element of the carrier of X
y1 \ x1 is Element of the carrier of X
the InternalDiff of X . (y1,x1) is Element of the carrier of X
((y1 \ y1) \ (x1 \ y1)) \ (y1 \ x1) is Element of the carrier of X
the InternalDiff of X . (((y1 \ y1) \ (x1 \ y1)),(y1 \ x1)) is Element of the carrier of X
0. X is V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
y1 \ y1 is Element of the carrier of X
the InternalDiff of X . (y1,y1) is Element of the carrier of X
y1 \ x1 is Element of the carrier of X
the InternalDiff of X . (y1,x1) is Element of the carrier of X
(y1 \ y1) \ (y1 \ x1) is Element of the carrier of X
the InternalDiff of X . ((y1 \ y1),(y1 \ x1)) is Element of the carrier of X
x1 \ y1 is Element of the carrier of X
the InternalDiff of X . (x1,y1) is Element of the carrier of X
((y1 \ y1) \ (y1 \ x1)) \ (x1 \ y1) is Element of the carrier of X
the InternalDiff of X . (((y1 \ y1) \ (y1 \ x1)),(x1 \ y1)) is Element of the carrier of X
w1 is set
x1 is set
[w1,x1] is set
{w1,x1} is set
{w1} is set
{{w1,x1},{w1}} is set
[x1,w1] is set
{x1,w1} is set
{x1} is set
{{x1,w1},{x1}} is set
x1 is Element of the carrier of X
y1 is Element of the carrier of X
x1 \ y1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (x1,y1) is Element of the carrier of X
y1 \ x1 is Element of the carrier of X
the InternalDiff of X . (y1,x1) is Element of the carrier of X
RI is Relation-like the carrier of X -defined the carrier of X -valued (X,I)
IT is Relation-like the carrier of X -defined the carrier of X -valued (X,I)
w1 is Relation-like the carrier of X -defined the carrier of X -valued (X,I)
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
[: the carrier of X, the carrier of X:] is non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
I is set
RI is set
IT is non empty Ideal of X
I is set
RI is set
IT is set
w1 is set
x1 is non empty Ideal of X
IT is set
w1 is set
x1 is non empty Ideal of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
{ b1 where b1 is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X) : verum } is set
{ b1 where b1 is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X) : verum } is set
{ b1 where b1 is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X) : verum } 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 V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X)
Class (I,(0. X)) is Element of bool the carrier of X
bool the carrier of X is non empty set
{(0. X)} is set
I .: {(0. X)} is set
RI is Element of the carrier of X
IT is Element of the carrier of X
RI \ IT is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (RI,IT) is Element of the carrier of X
[RI,RI] is set
{RI,RI} is set
{RI} is set
{{RI,RI},{RI}} is set
[(0. X),IT] is set
{(0. X),IT} is set
{{(0. X),IT},{(0. X)}} is set
RI \ (0. X) is Element of the carrier of X
the InternalDiff of X . (RI,(0. X)) is Element of the carrier of X
[(RI \ (0. X)),(RI \ IT)] is set
{(RI \ (0. X)),(RI \ IT)} is set
{(RI \ (0. X))} is set
{{(RI \ (0. X)),(RI \ IT)},{(RI \ (0. X))}} is set
[RI,(RI \ IT)] is set
{RI,(RI \ IT)} is set
{{RI,(RI \ IT)},{RI}} is set
[(RI \ IT),RI] is set
{(RI \ IT),RI} is set
{(RI \ IT)} is set
{{(RI \ IT),RI},{(RI \ IT)}} is set
[(0. X),(RI \ IT)] is set
{(0. X),(RI \ IT)} is set
{{(0. X),(RI \ IT)},{(0. X)}} is set
[(0. X),RI] is set
{(0. X),RI} is set
{{(0. X),RI},{(0. X)}} is set
[(0. X),(0. X)] is set
{(0. X),(0. X)} is set
{{(0. X),(0. X)},{(0. X)}} is set
RI is non empty Ideal of X
IT is Element of RI
[(0. X),IT] is set
{(0. X),IT} is set
{{(0. X),IT},{(0. 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
IT ` is Element of the carrier of X
(0. X) \ IT is Element of the carrier of X
the InternalDiff of X . ((0. X),IT) is Element of the carrier of X
[((0. X) `),(IT `)] is set
{((0. X) `),(IT `)} is set
{((0. X) `)} is set
{{((0. X) `),(IT `)},{((0. X) `)}} is set
[(0. X),(IT `)] is set
{(0. X),(IT `)} is set
{{(0. X),(IT `)},{(0. X)}} 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
[: the carrier of X, the carrier of X:] is non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
I is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive Element of bool [: the carrier of X, the carrier of X:]
field I is set
dom I is set
rng I is set
(dom I) \/ (rng I) is set
RI is Element of the carrier of X
IT is Element of the carrier of X
[RI,IT] is set
{RI,IT} is set
{RI} is set
{{RI,IT},{RI}} is set
w1 is Element of the carrier of X
RI \ w1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (RI,w1) is Element of the carrier of X
IT \ w1 is Element of the carrier of X
the InternalDiff of X . (IT,w1) is Element of the carrier of X
[(RI \ w1),(IT \ w1)] is set
{(RI \ w1),(IT \ w1)} is set
{(RI \ w1)} is set
{{(RI \ w1),(IT \ w1)},{(RI \ w1)}} is set
[w1,w1] is set
{w1,w1} is set
{w1} is set
{{w1,w1},{w1}} is set
RI is Element of the carrier of X
IT is Element of the carrier of X
[RI,IT] is set
{RI,IT} is set
{RI} is set
{{RI,IT},{RI}} is set
w1 is Element of the carrier of X
w1 \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (w1,RI) is Element of the carrier of X
w1 \ IT is Element of the carrier of X
the InternalDiff of X . (w1,IT) is Element of the carrier of X
[(w1 \ RI),(w1 \ IT)] is set
{(w1 \ RI),(w1 \ IT)} is set
{(w1 \ RI)} is set
{{(w1 \ RI),(w1 \ IT)},{(w1 \ RI)}} is set
[w1,w1] is set
{w1,w1} is set
{w1} is set
{{w1,w1},{w1}} is set
RI is Element of the carrier of X
IT is Element of the carrier of X
[RI,IT] is set
{RI,IT} is set
{RI} is set
{{RI,IT},{RI}} is set
w1 is Element of the carrier of X
x1 is Element of the carrier of X
[w1,x1] is set
{w1,x1} is set
{w1} is set
{{w1,x1},{w1}} is set
RI \ w1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (RI,w1) is Element of the carrier of X
IT \ w1 is Element of the carrier of X
the InternalDiff of X . (IT,w1) is Element of the carrier of X
[(RI \ w1),(IT \ w1)] is set
{(RI \ w1),(IT \ w1)} is set
{(RI \ w1)} is set
{{(RI \ w1),(IT \ w1)},{(RI \ w1)}} is set
IT \ x1 is Element of the carrier of X
the InternalDiff of X . (IT,x1) is Element of the carrier of X
[(IT \ w1),(IT \ x1)] is set
{(IT \ w1),(IT \ x1)} is set
{(IT \ w1)} is set
{{(IT \ w1),(IT \ x1)},{(IT \ w1)}} is set
[(RI \ w1),(IT \ x1)] is set
{(RI \ w1),(IT \ x1)} is set
{{(RI \ w1),(IT \ x1)},{(RI \ w1)}} 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
I is non empty Ideal of X
RI is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X,I)
field RI is set
dom RI is set
rng RI is set
(dom RI) \/ (rng RI) is set
IT is Element of the carrier of X
w1 is Element of the carrier of X
[IT,w1] is set
{IT,w1} is set
{IT} is set
{{IT,w1},{IT}} is set
x1 is Element of the carrier of X
x1 is Element of the carrier of X
[x1,x1] is set
{x1,x1} is set
{x1} is set
{{x1,x1},{x1}} is set
w1 \ x1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (w1,x1) is Element of the carrier of X
w1 \ x1 is Element of the carrier of X
the InternalDiff of X . (w1,x1) is Element of the carrier of X
(w1 \ x1) \ (w1 \ x1) is Element of the carrier of X
the InternalDiff of X . ((w1 \ x1),(w1 \ x1)) is Element of the carrier of X
x1 \ x1 is Element of the carrier of X
the InternalDiff of X . (x1,x1) is Element of the carrier of X
((w1 \ x1) \ (w1 \ x1)) \ (x1 \ x1) is Element of the carrier of X
the InternalDiff of X . (((w1 \ x1) \ (w1 \ x1)),(x1 \ x1)) is Element of the carrier of X
0. X is V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
(w1 \ x1) \ (w1 \ x1) is Element of the carrier of X
the InternalDiff of X . ((w1 \ x1),(w1 \ x1)) is Element of the carrier of X
x1 \ x1 is Element of the carrier of X
the InternalDiff of X . (x1,x1) is Element of the carrier of X
((w1 \ x1) \ (w1 \ x1)) \ (x1 \ x1) is Element of the carrier of X
the InternalDiff of X . (((w1 \ x1) \ (w1 \ x1)),(x1 \ x1)) is Element of the carrier of X
[(w1 \ x1),(w1 \ x1)] is set
{(w1 \ x1),(w1 \ x1)} is set
{(w1 \ x1)} is set
{{(w1 \ x1),(w1 \ x1)},{(w1 \ x1)}} is set
IT \ x1 is Element of the carrier of X
the InternalDiff of X . (IT,x1) is Element of the carrier of X
(IT \ x1) \ (w1 \ x1) is Element of the carrier of X
the InternalDiff of X . ((IT \ x1),(w1 \ x1)) is Element of the carrier of X
IT \ w1 is Element of the carrier of X
the InternalDiff of X . (IT,w1) is Element of the carrier of X
((IT \ x1) \ (w1 \ x1)) \ (IT \ w1) is Element of the carrier of X
the InternalDiff of X . (((IT \ x1) \ (w1 \ x1)),(IT \ w1)) is Element of the carrier of X
(w1 \ x1) \ (IT \ x1) is Element of the carrier of X
the InternalDiff of X . ((w1 \ x1),(IT \ x1)) is Element of the carrier of X
w1 \ IT is Element of the carrier of X
the InternalDiff of X . (w1,IT) is Element of the carrier of X
((w1 \ x1) \ (IT \ x1)) \ (w1 \ IT) is Element of the carrier of X
the InternalDiff of X . (((w1 \ x1) \ (IT \ x1)),(w1 \ IT)) is Element of the carrier of X
[(IT \ x1),(w1 \ x1)] is set
{(IT \ x1),(w1 \ x1)} is set
{(IT \ x1)} is set
{{(IT \ x1),(w1 \ x1)},{(IT \ x1)}} is set
[(IT \ x1),(w1 \ x1)] is set
{(IT \ x1),(w1 \ x1)} is set
{{(IT \ x1),(w1 \ x1)},{(IT \ x1)}} 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
I is non empty Ideal of X
RI is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X,I)
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 V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is non empty Ideal of X
RI is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X,I)
Class (RI,(0. X)) is Element of bool the carrier of X
bool the carrier of X is non empty set
{(0. X)} is set
RI .: {(0. X)} is set
IT is set
w1 is set
[w1,IT] is set
{w1,IT} is set
{w1} is set
{{w1,IT},{w1}} is set
x1 is Element of the carrier of X
x1 is Element of the carrier of X
x1 \ (0. X) is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (x1,(0. X)) is Element of the carrier of X
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 V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is non empty Ideal of X
RI is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X,I)
Class (RI,(0. X)) is Element of bool the carrier of X
bool the carrier of X is non empty set
{(0. X)} is set
RI .: {(0. X)} is set
IT is set
w1 is Element of I
w1 \ (0. X) is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (w1,(0. X)) is Element of the carrier of X
w1 ` is Element of the carrier of X
(0. X) \ w1 is Element of the carrier of X
the InternalDiff of X . ((0. X),w1) is Element of the carrier of X
[(0. X),w1] is set
{(0. X),w1} is set
{{(0. X),w1},{(0. X)}} is set
IT is Element of I
[(0. X),IT] is set
{(0. X),IT} is set
{{(0. X),IT},{(0. X)}} is set
w1 is set
[w1,IT] is set
{w1,IT} is set
{w1} is set
{{w1,IT},{w1}} is set
IT ` is Element of the carrier of X
(0. X) \ IT is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),IT) is Element of the carrier of X
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 V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
RI is Element of the carrier of X
[I,RI] is set
{I,RI} is set
{I} is set
{{I,RI},{I}} is set
I \ RI is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (I,RI) is Element of the carrier of X
RI \ I is Element of the carrier of X
the InternalDiff of X . (RI,I) is Element of the carrier of X
IT is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X)
Class (IT,(0. X)) is Element of bool the carrier of X
bool the carrier of X is non empty set
{(0. X)} is set
IT .: {(0. X)} is set
field IT is set
dom IT is set
rng IT is set
(dom IT) \/ (rng IT) is set
[RI,RI] is set
{RI,RI} is set
{RI} is set
{{RI,RI},{RI}} is set
[RI,I] is set
{RI,I} is set
{{RI,I},{RI}} is set
RI \ RI is Element of the carrier of X
the InternalDiff of X . (RI,RI) is Element of the carrier of X
[(RI \ RI),(I \ RI)] is set
{(RI \ RI),(I \ RI)} is set
{(RI \ RI)} is set
{{(RI \ RI),(I \ RI)},{(RI \ RI)}} is set
[(0. X),(I \ RI)] is set
{(0. X),(I \ RI)} is set
{{(0. X),(I \ RI)},{(0. X)}} is set
[I,I] is set
{I,I} is set
{{I,I},{I}} is set
I \ I is Element of the carrier of X
the InternalDiff of X . (I,I) is Element of the carrier of X
[(I \ I),(RI \ I)] is set
{(I \ I),(RI \ I)} is set
{(I \ I)} is set
{{(I \ I),(RI \ I)},{(I \ I)}} is set
[(0. X),(RI \ I)] is set
{(0. X),(RI \ I)} is set
{{(0. X),(RI \ I)},{(0. X)}} 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 V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is non empty Ideal of X
RI is non empty Ideal of X
IT is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X,I)
Class (IT,(0. X)) is Element of bool the carrier of X
bool the carrier of X is non empty set
{(0. X)} is set
IT .: {(0. X)} is set
w1 is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X,RI)
Class (w1,(0. X)) is Element of bool the carrier of X
w1 .: {(0. X)} is set
x1 is set
x1 is set
[x1,x1] is set
{x1,x1} is set
{x1} is set
{{x1,x1},{x1}} is set
y1 is set
x1 is set
[y1,x1] is set
{y1,x1} is set
{y1} is set
{{y1,x1},{y1}} is set
y1 is Element of the carrier of X
x1 is Element of the carrier of X
y1 \ x1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (y1,x1) is Element of the carrier of X
[(0. X),(y1 \ x1)] is set
{(0. X),(y1 \ x1)} is set
{{(0. X),(y1 \ x1)},{(0. X)}} is set
y1 is set
[y1,(y1 \ x1)] is set
{y1,(y1 \ x1)} is set
{y1} is set
{{y1,(y1 \ x1)},{y1}} is set
(y1 \ x1) \ (0. X) is Element of the carrier of X
the InternalDiff of X . ((y1 \ x1),(0. X)) is Element of the carrier of X
x1 \ y1 is Element of the carrier of X
the InternalDiff of X . (x1,y1) is Element of the carrier of X
[(0. X),(x1 \ y1)] is set
{(0. X),(x1 \ y1)} is set
{{(0. X),(x1 \ y1)},{(0. X)}} is set
y1 is set
[y1,(x1 \ y1)] is set
{y1,(x1 \ y1)} is set
{y1} is set
{{y1,(x1 \ y1)},{y1}} is set
(x1 \ y1) \ (0. X) is Element of the carrier of X
the InternalDiff of X . ((x1 \ y1),(0. X)) is Element of the carrier of X
y1 is set
x1 is set
[y1,x1] is set
{y1,x1} is set
{y1} is set
{{y1,x1},{y1}} is set
y1 is Element of the carrier of X
x1 is Element of the carrier of X
y1 \ x1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (y1,x1) is Element of the carrier of X
[(0. X),(y1 \ x1)] is set
{(0. X),(y1 \ x1)} is set
{{(0. X),(y1 \ x1)},{(0. X)}} is set
y1 is set
[y1,(y1 \ x1)] is set
{y1,(y1 \ x1)} is set
{y1} is set
{{y1,(y1 \ x1)},{y1}} is set
(y1 \ x1) \ (0. X) is Element of the carrier of X
the InternalDiff of X . ((y1 \ x1),(0. X)) is Element of the carrier of X
x1 \ y1 is Element of the carrier of X
the InternalDiff of X . (x1,y1) is Element of the carrier of X
[(0. X),(x1 \ y1)] is set
{(0. X),(x1 \ y1)} is set
{{(0. X),(x1 \ y1)},{(0. X)}} is set
y1 is set
[y1,(x1 \ y1)] is set
{y1,(x1 \ y1)} is set
{y1} is set
{{y1,(x1 \ y1)},{y1}} is set
(x1 \ y1) \ (0. X) is Element of the carrier of X
the InternalDiff of X . ((x1 \ y1),(0. X)) is Element of the carrier of X
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 V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Element of the carrier of X
RI is Element of the carrier of X
[I,RI] is set
{I,RI} is set
{I} is set
{{I,RI},{I}} is set
IT is Element of the carrier of X
w1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,RI,IT,w1) is Element of the carrier of X
[I,(X,RI,IT,w1)] is set
{I,(X,RI,IT,w1)} is set
{{I,(X,RI,IT,w1)},{I}} is set
x1 is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X)
Class (x1,(0. X)) is Element of bool the carrier of X
bool the carrier of X is non empty set
{(0. X)} is set
x1 .: {(0. X)} is set
[(0. X),IT] is set
{(0. X),IT} is set
{{(0. X),IT},{(0. X)}} is set
x1 is set
[x1,IT] is set
{x1,IT} is set
{x1} is set
{{x1,IT},{x1}} is set
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,RI,IT,x1) is Element of the carrier of X
[I,(X,RI,IT,x1)] is set
{I,(X,RI,IT,x1)} is set
{{I,(X,RI,IT,x1)},{I}} is set
x1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,RI,IT,(x1 + 1)) is Element of the carrier of X
[I,(X,RI,IT,(x1 + 1))] is set
{I,(X,RI,IT,(x1 + 1))} is set
{{I,(X,RI,IT,(x1 + 1))},{I}} is set
I \ (0. X) is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (I,(0. X)) is Element of the carrier of X
(X,RI,IT,x1) \ IT is Element of the carrier of X
the InternalDiff of X . ((X,RI,IT,x1),IT) is Element of the carrier of X
[(I \ (0. X)),((X,RI,IT,x1) \ IT)] is set
{(I \ (0. X)),((X,RI,IT,x1) \ IT)} is set
{(I \ (0. X))} is set
{{(I \ (0. X)),((X,RI,IT,x1) \ IT)},{(I \ (0. X))}} is set
[I,((X,RI,IT,x1) \ IT)] is set
{I,((X,RI,IT,x1) \ IT)} is set
{{I,((X,RI,IT,x1) \ IT)},{I}} is set
(X,RI,IT,0) is Element of the carrier of X
[I,(X,RI,IT,0)] is set
{I,(X,RI,IT,0)} is set
{{I,(X,RI,IT,0)},{I}} 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 V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X)
Class (I,(0. X)) is Element of bool the carrier of X
bool the carrier of X is non empty set
{(0. X)} is set
I .: {(0. X)} is set
RI is non empty Ideal of X
IT is Element of the carrier of X
w1 is Element of the carrier of X
IT \ w1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (IT,w1) is Element of the carrier of X
w1 \ IT is Element of the carrier of X
the InternalDiff of X . (w1,IT) is Element of the carrier of X
[IT,w1] is set
{IT,w1} is set
{IT} is set
{{IT,w1},{IT}} is set
[(0. X),(w1 \ IT)] is set
{(0. X),(w1 \ IT)} is set
{{(0. X),(w1 \ IT)},{(0. X)}} is set
x1 is set
[x1,(w1 \ IT)] is set
{x1,(w1 \ IT)} is set
{x1} is set
{{x1,(w1 \ IT)},{x1}} is set
[(0. X),(IT \ w1)] is set
{(0. X),(IT \ w1)} is set
{{(0. X),(IT \ w1)},{(0. X)}} is set
x1 is set
[x1,(IT \ w1)] is set
{x1,(IT \ w1)} is set
{x1} is set
{{x1,(IT \ w1)},{x1}} is set
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,IT,(IT \ w1),x1) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(X,IT,(IT \ w1),x1),(w1 \ IT),x1) is Element of the carrier of X
y1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,w1,(w1 \ IT),y1) is Element of the carrier of X
x1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(X,w1,(w1 \ IT),y1),(IT \ w1),x1) is Element of the carrier of X
field I is set
dom I is set
rng I is set
(dom I) \/ (rng I) is set
[IT,IT] is set
{IT,IT} is set
{{IT,IT},{IT}} is set
[IT,(X,IT,(IT \ w1),x1)] is set
{IT,(X,IT,(IT \ w1),x1)} is set
{{IT,(X,IT,(IT \ w1),x1)},{IT}} is set
[IT,(X,(X,IT,(IT \ w1),x1),(w1 \ IT),x1)] is set
{IT,(X,(X,IT,(IT \ w1),x1),(w1 \ IT),x1)} is set
{{IT,(X,(X,IT,(IT \ w1),x1),(w1 \ IT),x1)},{IT}} is set
y1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(X,IT,(IT \ w1),x1),(w1 \ IT),y1) is Element of the carrier of X
[IT,(X,(X,IT,(IT \ w1),x1),(w1 \ IT),y1)] is set
{IT,(X,(X,IT,(IT \ w1),x1),(w1 \ IT),y1)} is set
{{IT,(X,(X,IT,(IT \ w1),x1),(w1 \ IT),y1)},{IT}} is set
y1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(X,IT,(IT \ w1),x1),(w1 \ IT),(y1 + 1)) is Element of the carrier of X
[IT,(X,(X,IT,(IT \ w1),x1),(w1 \ IT),(y1 + 1))] is set
{IT,(X,(X,IT,(IT \ w1),x1),(w1 \ IT),(y1 + 1))} is set
{{IT,(X,(X,IT,(IT \ w1),x1),(w1 \ IT),(y1 + 1))},{IT}} is set
IT \ (0. X) is Element of the carrier of X
the InternalDiff of X . (IT,(0. X)) is Element of the carrier of X
(X,(X,IT,(IT \ w1),x1),(w1 \ IT),y1) \ (w1 \ IT) is Element of the carrier of X
the InternalDiff of X . ((X,(X,IT,(IT \ w1),x1),(w1 \ IT),y1),(w1 \ IT)) is Element of the carrier of X
[(IT \ (0. X)),((X,(X,IT,(IT \ w1),x1),(w1 \ IT),y1) \ (w1 \ IT))] is set
{(IT \ (0. X)),((X,(X,IT,(IT \ w1),x1),(w1 \ IT),y1) \ (w1 \ IT))} is set
{(IT \ (0. X))} is set
{{(IT \ (0. X)),((X,(X,IT,(IT \ w1),x1),(w1 \ IT),y1) \ (w1 \ IT))},{(IT \ (0. X))}} is set
[IT,((X,(X,IT,(IT \ w1),x1),(w1 \ IT),y1) \ (w1 \ IT))] is set
{IT,((X,(X,IT,(IT \ w1),x1),(w1 \ IT),y1) \ (w1 \ IT))} is set
{{IT,((X,(X,IT,(IT \ w1),x1),(w1 \ IT),y1) \ (w1 \ IT))},{IT}} is set
(X,(X,IT,(IT \ w1),x1),(w1 \ IT),0) is Element of the carrier of X
[IT,(X,(X,IT,(IT \ w1),x1),(w1 \ IT),0)] is set
{IT,(X,(X,IT,(IT \ w1),x1),(w1 \ IT),0)} is set
{{IT,(X,(X,IT,(IT \ w1),x1),(w1 \ IT),0)},{IT}} is set
[w1,w1] is set
{w1,w1} is set
{w1} is set
{{w1,w1},{w1}} is set
[w1,(X,w1,(w1 \ IT),y1)] is set
{w1,(X,w1,(w1 \ IT),y1)} is set
{{w1,(X,w1,(w1 \ IT),y1)},{w1}} is set
[w1,(X,(X,w1,(w1 \ IT),y1),(IT \ w1),x1)] is set
{w1,(X,(X,w1,(w1 \ IT),y1),(IT \ w1),x1)} is set
{{w1,(X,(X,w1,(w1 \ IT),y1),(IT \ w1),x1)},{w1}} is set
y1 is V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(X,w1,(w1 \ IT),y1),(IT \ w1),y1) is Element of the carrier of X
[w1,(X,(X,w1,(w1 \ IT),y1),(IT \ w1),y1)] is set
{w1,(X,(X,w1,(w1 \ IT),y1),(IT \ w1),y1)} is set
{{w1,(X,(X,w1,(w1 \ IT),y1),(IT \ w1),y1)},{w1}} is set
y1 + 1 is non empty V21() V22() V23() V27() V74() ext-real non negative V78() Element of NAT
(X,(X,w1,(w1 \ IT),y1),(IT \ w1),(y1 + 1)) is Element of the carrier of X
[w1,(X,(X,w1,(w1 \ IT),y1),(IT \ w1),(y1 + 1))] is set
{w1,(X,(X,w1,(w1 \ IT),y1),(IT \ w1),(y1 + 1))} is set
{{w1,(X,(X,w1,(w1 \ IT),y1),(IT \ w1),(y1 + 1))},{w1}} is set
w1 \ (0. X) is Element of the carrier of X
the InternalDiff of X . (w1,(0. X)) is Element of the carrier of X
(X,(X,w1,(w1 \ IT),y1),(IT \ w1),y1) \ (IT \ w1) is Element of the carrier of X
the InternalDiff of X . ((X,(X,w1,(w1 \ IT),y1),(IT \ w1),y1),(IT \ w1)) is Element of the carrier of X
[(w1 \ (0. X)),((X,(X,w1,(w1 \ IT),y1),(IT \ w1),y1) \ (IT \ w1))] is set
{(w1 \ (0. X)),((X,(X,w1,(w1 \ IT),y1),(IT \ w1),y1) \ (IT \ w1))} is set
{(w1 \ (0. X))} is set
{{(w1 \ (0. X)),((X,(X,w1,(w1 \ IT),y1),(IT \ w1),y1) \ (IT \ w1))},{(w1 \ (0. X))}} is set
[w1,((X,(X,w1,(w1 \ IT),y1),(IT \ w1),y1) \ (IT \ w1))] is set
{w1,((X,(X,w1,(w1 \ IT),y1),(IT \ w1),y1) \ (IT \ w1))} is set
{{w1,((X,(X,w1,(w1 \ IT),y1),(IT \ w1),y1) \ (IT \ w1))},{w1}} is set
(X,(X,w1,(w1 \ IT),y1),(IT \ w1),0) is Element of the carrier of X
[w1,(X,(X,w1,(w1 \ IT),y1),(IT \ w1),0)] is set
{w1,(X,(X,w1,(w1 \ IT),y1),(IT \ w1),0)} is set
{{w1,(X,(X,w1,(w1 \ IT),y1),(IT \ w1),0)},{w1}} is set
[(X,(X,IT,(IT \ w1),x1),(w1 \ IT),x1),w1] is set
{(X,(X,IT,(IT \ w1),x1),(w1 \ IT),x1),w1} is set
{(X,(X,IT,(IT \ w1),x1),(w1 \ IT),x1)} is set
{{(X,(X,IT,(IT \ w1),x1),(w1 \ IT),x1),w1},{(X,(X,IT,(IT \ w1),x1),(w1 \ IT),x1)}} is set
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
(X) is set
(X) is set
the carrier of X is non empty set
{ b1 where b1 is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X) : verum } is set
I is set
RI is non empty Ideal of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
(X) is set
the carrier of X is non empty set
{ b1 where b1 is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X) : verum } is set
(X) is set
{ b1 where b1 is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X) : verum } is set
I is set
RI is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X)
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
(X) is set
the carrier of X is non empty set
{ b1 where b1 is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X) : verum } is set
(X) is set
{ b1 where b1 is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X) : verum } is set
I is set
RI is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X)
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
(X) is set
the carrier of X is non empty set
{ b1 where b1 is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X) : verum } is set
(X) is set
{ b1 where b1 is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X) : verum } is set
(X) is set
{ b1 where b1 is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X) : verum } is set
(X) /\ (X) is set
I is set
RI is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X)
IT is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X)
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is non empty Ideal of X
RI is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X,I)
IT is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X)
w1 is set
x1 is set
[w1,x1] is set
{w1,x1} is set
{w1} is set
{{w1,x1},{w1}} is set
x1 is set
y1 is set
[x1,y1] is set
{x1,y1} is set
{x1} is set
{{x1,y1},{x1}} is set
y1 is Element of the carrier of X
x1 is Element of the carrier of X
y1 \ x1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (y1,x1) is Element of the carrier of X
0. X is V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
Class (IT,(0. X)) is Element of bool the carrier of X
bool the carrier of X is non empty set
{(0. X)} is set
IT .: {(0. X)} is set
[(0. X),(y1 \ x1)] is set
{(0. X),(y1 \ x1)} is set
{{(0. X),(y1 \ x1)},{(0. X)}} is set
x1 is set
[x1,(y1 \ x1)] is set
{x1,(y1 \ x1)} is set
{x1} is set
{{x1,(y1 \ x1)},{x1}} is set
(y1 \ x1) \ (0. X) is Element of the carrier of X
the InternalDiff of X . ((y1 \ x1),(0. X)) is Element of the carrier of X
x1 \ y1 is Element of the carrier of X
the InternalDiff of X . (x1,y1) is Element of the carrier of X
[(0. X),(x1 \ y1)] is set
{(0. X),(x1 \ y1)} is set
{{(0. X),(x1 \ y1)},{(0. X)}} is set
x1 is set
[x1,(x1 \ y1)] is set
{x1,(x1 \ y1)} is set
{x1} is set
{{x1,(x1 \ y1)},{x1}} is set
(x1 \ y1) \ (0. X) is Element of the carrier of X
the InternalDiff of X . ((x1 \ y1),(0. X)) is Element of the carrier of X
x1 is set
y1 is set
[x1,y1] is set
{x1,y1} is set
{x1} is set
{{x1,y1},{x1}} is set
x1 is Element of the carrier of X
y1 is Element of the carrier of X
x1 \ y1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (x1,y1) is Element of the carrier of X
y1 \ x1 is Element of the carrier of X
the InternalDiff of X . (y1,x1) is Element of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is non empty Ideal of X
RI is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X,I)
IT is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X)
w1 is set
x1 is set
[w1,x1] is set
{w1,x1} is set
{w1} is set
{{w1,x1},{w1}} is set
x1 is set
y1 is set
[x1,y1] is set
{x1,y1} is set
{x1} is set
{{x1,y1},{x1}} is set
y1 is Element of the carrier of X
x1 is Element of the carrier of X
y1 \ x1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (y1,x1) is Element of the carrier of X
0. X is V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
Class (IT,(0. X)) is Element of bool the carrier of X
bool the carrier of X is non empty set
{(0. X)} is set
IT .: {(0. X)} is set
[(0. X),(y1 \ x1)] is set
{(0. X),(y1 \ x1)} is set
{{(0. X),(y1 \ x1)},{(0. X)}} is set
x1 is set
[x1,(y1 \ x1)] is set
{x1,(y1 \ x1)} is set
{x1} is set
{{x1,(y1 \ x1)},{x1}} is set
(y1 \ x1) \ (0. X) is Element of the carrier of X
the InternalDiff of X . ((y1 \ x1),(0. X)) is Element of the carrier of X
x1 \ y1 is Element of the carrier of X
the InternalDiff of X . (x1,y1) is Element of the carrier of X
[(0. X),(x1 \ y1)] is set
{(0. X),(x1 \ y1)} is set
{{(0. X),(x1 \ y1)},{(0. X)}} is set
x1 is set
[x1,(x1 \ y1)] is set
{x1,(x1 \ y1)} is set
{x1} is set
{{x1,(x1 \ y1)},{x1}} is set
(x1 \ y1) \ (0. X) is Element of the carrier of X
the InternalDiff of X . ((x1 \ y1),(0. X)) is Element of the carrier of X
x1 is set
y1 is set
[x1,y1] is set
{x1,y1} is set
{x1} is set
{{x1,y1},{x1}} is set
x1 is Element of the carrier of X
y1 is Element of the carrier of X
x1 \ y1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (x1,y1) is Element of the carrier of X
y1 \ x1 is Element of the carrier of X
the InternalDiff of X . (y1,x1) is Element of the carrier of X
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 V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
I is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X)
Class (I,(0. X)) is Element of bool the carrier of X
bool the carrier of X is non empty set
{(0. X)} is set
I .: {(0. X)} is set
RI is Element of the carrier of X
IT is Element of the carrier of X
RI \ IT is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (RI,IT) is Element of the carrier of X
[(0. X),IT] is set
{(0. X),IT} is set
{{(0. X),IT},{(0. X)}} is set
RI \ (0. X) is Element of the carrier of X
the InternalDiff of X . (RI,(0. X)) is Element of the carrier of X
[(RI \ (0. X)),(RI \ IT)] is set
{(RI \ (0. X)),(RI \ IT)} is set
{(RI \ (0. X))} is set
{{(RI \ (0. X)),(RI \ IT)},{(RI \ (0. X))}} is set
[RI,(RI \ IT)] is set
{RI,(RI \ IT)} is set
{RI} is set
{{RI,(RI \ IT)},{RI}} is set
[(RI \ IT),RI] is set
{(RI \ IT),RI} is set
{(RI \ IT)} is set
{{(RI \ IT),RI},{(RI \ IT)}} is set
[(0. X),(RI \ IT)] is set
{(0. X),(RI \ IT)} is set
{{(0. X),(RI \ IT)},{(0. X)}} is set
[(0. X),RI] is set
{(0. X),RI} is set
{{(0. X),RI},{(0. X)}} is set
[(0. X),(0. X)] is set
{(0. X),(0. X)} is set
{{(0. X),(0. X)},{(0. X)}} is set
RI is non empty Ideal of X
IT is Element of RI
[(0. X),IT] is set
{(0. X),IT} is set
{{(0. X),IT},{(0. 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
IT ` is Element of the carrier of X
(0. X) \ IT is Element of the carrier of X
the InternalDiff of X . ((0. X),IT) is Element of the carrier of X
[((0. X) `),(IT `)] is set
{((0. X) `),(IT `)} is set
{((0. X) `)} is set
{{((0. X) `),(IT `)},{((0. X) `)}} is set
[(0. X),(IT `)] is set
{(0. X),(IT `)} is set
{{(0. X),(IT `)},{(0. X)}} 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
I is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X)
Class I is a_partition of the carrier of X
0. X is V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
Class (I,(0. X)) is Element of bool the carrier of X
bool the carrier of X is non empty set
{(0. X)} is set
I .: {(0. X)} 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
I is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X)
Class I is non empty a_partition of the carrier of X
[:(Class I),(Class I):] is non empty set
[:[:(Class I),(Class I):],(Class I):] is non empty set
bool [:[:(Class I),(Class I):],(Class I):] is non empty set
bool the carrier of X is non empty set
RI is Element of Class I
IT is Element of Class I
w1 is set
Class (I,w1) is Element of bool the carrier of X
{w1} is set
I .: {w1} is set
x1 is set
Class (I,x1) is Element of bool the carrier of X
{x1} is set
I .: {x1} is set
x1 is Element of the carrier of X
y1 is Element of the carrier of X
x1 \ y1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (x1,y1) is Element of the carrier of X
Class (I,(x1 \ y1)) is Element of bool the carrier of X
{(x1 \ y1)} is set
I .: {(x1 \ y1)} is set
x1 is Element of Class I
y1 is Element of the carrier of X
Class (I,y1) is Element of bool the carrier of X
{y1} is set
I .: {y1} is set
x1 is Element of the carrier of X
Class (I,x1) is Element of bool the carrier of X
{x1} is set
I .: {x1} is set
Class (I,y1) is Element of bool the carrier of X
{y1} is set
I .: {y1} is set
[y1,x1] is set
{y1,x1} is set
{{y1,x1},{y1}} is set
Class (I,x1) is Element of bool the carrier of X
{x1} is set
I .: {x1} is set
[x1,y1] is set
{x1,y1} is set
{{x1,y1},{x1}} is set
y1 \ x1 is Element of the carrier of X
the InternalDiff of X . (y1,x1) is Element of the carrier of X
[(x1 \ y1),(y1 \ x1)] is set
{(x1 \ y1),(y1 \ x1)} is set
{{(x1 \ y1),(y1 \ x1)},{(x1 \ y1)}} is set
Class (I,(y1 \ x1)) is Element of bool the carrier of X
{(y1 \ x1)} is set
I .: {(y1 \ x1)} is set
y1 is Element of the carrier of X
Class (I,y1) is Element of bool the carrier of X
{y1} is set
I .: {y1} is set
x1 is Element of the carrier of X
Class (I,x1) is Element of bool the carrier of X
{x1} is set
I .: {x1} is set
y1 \ x1 is Element of the carrier of X
the InternalDiff of X . (y1,x1) is Element of the carrier of X
Class (I,(y1 \ x1)) is Element of bool the carrier of X
{(y1 \ x1)} is set
I .: {(y1 \ x1)} is set
RI is Relation-like [:(Class I),(Class I):] -defined Class I -valued Function-like V18([:(Class I),(Class I):], Class I) Element of bool [:[:(Class I),(Class I):],(Class I):]
IT is Relation-like [:(Class I),(Class I):] -defined Class I -valued Function-like V18([:(Class I),(Class I):], Class I) Element of bool [:[:(Class I),(Class I):],(Class I):]
w1 is Element of Class I
x1 is set
Class (I,x1) is Element of bool the carrier of X
{x1} is set
I .: {x1} is set
x1 is Element of Class I
y1 is set
Class (I,y1) is Element of bool the carrier of X
{y1} is set
I .: {y1} is set
RI . (w1,x1) is Element of Class I
x1 is Element of the carrier of X
y1 is Element of the carrier of X
x1 \ y1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (x1,y1) is Element of the carrier of X
Class (I,(x1 \ y1)) is Element of bool the carrier of X
{(x1 \ y1)} is set
I .: {(x1 \ y1)} is set
IT . (w1,x1) is Element of Class I
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X)
0. X is V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
Class (I,(0. X)) is Element of bool the carrier of X
bool the carrier of X is non empty set
{(0. X)} is set
I .: {(0. X)} is set
Class I is non empty a_partition of the carrier of X
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X)
Class I is non empty a_partition of the carrier of X
(X,I) is Relation-like [:(Class I),(Class I):] -defined Class I -valued Function-like V18([:(Class I),(Class I):], Class I) Element of bool [:[:(Class I),(Class I):],(Class I):]
[:(Class I),(Class I):] is non empty set
[:[:(Class I),(Class I):],(Class I):] is non empty set
bool [:[:(Class I),(Class I):],(Class I):] is non empty set
(X,I) is Element of Class I
bool the carrier of X is non empty set
0. X is V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
Class (I,(0. X)) is Element of bool the carrier of X
{(0. X)} is set
I .: {(0. X)} is set
BCIStr_0(# (Class I),(X,I),(X,I) #) is strict BCIStr_0
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X)
(X,I) is BCIStr_0
Class I is non empty a_partition of the carrier of X
(X,I) is Relation-like [:(Class I),(Class I):] -defined Class I -valued Function-like V18([:(Class I),(Class I):], Class I) Element of bool [:[:(Class I),(Class I):],(Class I):]
[:(Class I),(Class I):] is non empty set
[:[:(Class I),(Class I):],(Class I):] is non empty set
bool [:[:(Class I),(Class I):],(Class I):] is non empty set
(X,I) is Element of Class I
bool the carrier of X is non empty set
0. X is V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
Class (I,(0. X)) is Element of bool the carrier of X
{(0. X)} is set
I .: {(0. X)} is set
BCIStr_0(# (Class I),(X,I),(X,I) #) is strict BCIStr_0
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
bool the carrier of X is non empty set
I is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X)
Class I is non empty a_partition of the carrier of X
(X,I) is Relation-like [:(Class I),(Class I):] -defined Class I -valued Function-like V18([:(Class I),(Class I):], Class I) Element of bool [:[:(Class I),(Class I):],(Class I):]
[:(Class I),(Class I):] is non empty set
[:[:(Class I),(Class I):],(Class I):] is non empty set
bool [:[:(Class I),(Class I):],(Class I):] is non empty set
RI is Element of Class I
IT is Element of Class I
(X,I) . (RI,IT) is Element of Class I
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
the carrier of X is non empty set
I is non empty Ideal of X
RI is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X,I)
(X,RI) is non empty BCIStr_0
Class RI is non empty a_partition of the carrier of X
(X,RI) is Relation-like [:(Class RI),(Class RI):] -defined Class RI -valued Function-like V18([:(Class RI),(Class RI):], Class RI) Element of bool [:[:(Class RI),(Class RI):],(Class RI):]
[:(Class RI),(Class RI):] is non empty set
[:[:(Class RI),(Class RI):],(Class RI):] is non empty set
bool [:[:(Class RI),(Class RI):],(Class RI):] is non empty set
(X,RI) is Element of Class RI
bool the carrier of X is non empty set
0. X is V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
Class (RI,(0. X)) is Element of bool the carrier of X
{(0. X)} is set
RI .: {(0. X)} is set
BCIStr_0(# (Class RI),(X,RI),(X,RI) #) is strict BCIStr_0
IT is non empty BCIStr_0
the carrier of IT is non empty set
w1 is Element of the carrier of IT
y1 is set
Class (RI,y1) is Element of bool the carrier of X
{y1} is set
RI .: {y1} is set
x1 is Element of the carrier of IT
x1 is set
Class (RI,x1) is Element of bool the carrier of X
{x1} is set
RI .: {x1} is set
x1 is Element of the carrier of IT
y1 is set
Class (RI,y1) is Element of bool the carrier of X
{y1} is set
RI .: {y1} is set
x1 \ x1 is Element of the carrier of IT
the InternalDiff of IT is Relation-like [: the carrier of IT, the carrier of IT:] -defined the carrier of IT -valued Function-like V18([: the carrier of IT, the carrier of IT:], the carrier of IT) Element of bool [:[: the carrier of IT, the carrier of IT:], the carrier of IT:]
[: the carrier of IT, the carrier of IT:] is non empty set
[:[: the carrier of IT, the carrier of IT:], the carrier of IT:] is non empty set
bool [:[: the carrier of IT, the carrier of IT:], the carrier of IT:] is non empty set
the InternalDiff of IT . (x1,x1) is Element of the carrier of IT
z1 is Element of the carrier of X
y1 is Element of the carrier of X
z1 \ y1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . (z1,y1) is Element of the carrier of X
Class (RI,(z1 \ y1)) is Element of bool the carrier of X
{(z1 \ y1)} is set
RI .: {(z1 \ y1)} is set
w1 \ x1 is Element of the carrier of IT
the InternalDiff of IT . (w1,x1) is Element of the carrier of IT
x1 is Element of the carrier of X
x1 \ y1 is Element of the carrier of X
the InternalDiff of X . (x1,y1) is Element of the carrier of X
Class (RI,(x1 \ y1)) is Element of bool the carrier of X
{(x1 \ y1)} is set
RI .: {(x1 \ y1)} is set
(w1 \ x1) \ (x1 \ x1) is Element of the carrier of IT
the InternalDiff of IT . ((w1 \ x1),(x1 \ x1)) is Element of the carrier of IT
(x1 \ y1) \ (z1 \ y1) is Element of the carrier of X
the InternalDiff of X . ((x1 \ y1),(z1 \ y1)) is Element of the carrier of X
Class (RI,((x1 \ y1) \ (z1 \ y1))) is Element of bool the carrier of X
{((x1 \ y1) \ (z1 \ y1))} is set
RI .: {((x1 \ y1) \ (z1 \ y1))} is set
w1 \ x1 is Element of the carrier of IT
the InternalDiff of IT . (w1,x1) is Element of the carrier of IT
x1 \ z1 is Element of the carrier of X
the InternalDiff of X . (x1,z1) is Element of the carrier of X
Class (RI,(x1 \ z1)) is Element of bool the carrier of X
{(x1 \ z1)} is set
RI .: {(x1 \ z1)} is set
((w1 \ x1) \ (x1 \ x1)) \ (w1 \ x1) is Element of the carrier of IT
the InternalDiff of IT . (((w1 \ x1) \ (x1 \ x1)),(w1 \ x1)) is Element of the carrier of IT
((x1 \ y1) \ (z1 \ y1)) \ (x1 \ z1) is Element of the carrier of X
the InternalDiff of X . (((x1 \ y1) \ (z1 \ y1)),(x1 \ z1)) is Element of the carrier of X
Class (RI,(((x1 \ y1) \ (z1 \ y1)) \ (x1 \ z1))) is Element of bool the carrier of X
{(((x1 \ y1) \ (z1 \ y1)) \ (x1 \ z1))} is set
RI .: {(((x1 \ y1) \ (z1 \ y1)) \ (x1 \ z1))} is set
0. IT is V44(IT) Element of the carrier of IT
the ZeroF of IT is Element of the carrier of IT
w1 is Element of the carrier of IT
y1 is set
Class (RI,y1) is Element of bool the carrier of X
{y1} is set
RI .: {y1} is set
x1 is Element of the carrier of IT
x1 is set
Class (RI,x1) is Element of bool the carrier of X
{x1} is set
RI .: {x1} is set
x1 is Element of the carrier of IT
y1 is set
Class (RI,y1) is Element of bool the carrier of X
{y1} is set
RI .: {y1} is set
w1 \ x1 is Element of the carrier of IT
the InternalDiff of IT . (w1,x1) is Element of the carrier of IT
x1 is Element of the carrier of X
z1 is Element of the carrier of X
x1 \ z1 is Element of the carrier of X
the InternalDiff of X . (x1,z1) is Element of the carrier of X
Class (RI,(x1 \ z1)) is Element of bool the carrier of X
{(x1 \ z1)} is set
RI .: {(x1 \ z1)} is set
(w1 \ x1) \ x1 is Element of the carrier of IT
the InternalDiff of IT . ((w1 \ x1),x1) is Element of the carrier of IT
y1 is Element of the carrier of X
(x1 \ z1) \ y1 is Element of the carrier of X
the InternalDiff of X . ((x1 \ z1),y1) is Element of the carrier of X
Class (RI,((x1 \ z1) \ y1)) is Element of bool the carrier of X
{((x1 \ z1) \ y1)} is set
RI .: {((x1 \ z1) \ y1)} is set
w1 \ x1 is Element of the carrier of IT
the InternalDiff of IT . (w1,x1) is Element of the carrier of IT
x1 \ y1 is Element of the carrier of X
the InternalDiff of X . (x1,y1) is Element of the carrier of X
Class (RI,(x1 \ y1)) is Element of bool the carrier of X
{(x1 \ y1)} is set
RI .: {(x1 \ y1)} is set
(w1 \ x1) \ x1 is Element of the carrier of IT
the InternalDiff of IT . ((w1 \ x1),x1) is Element of the carrier of IT
(x1 \ y1) \ z1 is Element of the carrier of X
the InternalDiff of X . ((x1 \ y1),z1) is Element of the carrier of X
Class (RI,((x1 \ y1) \ z1)) is Element of bool the carrier of X
{((x1 \ y1) \ z1)} is set
RI .: {((x1 \ y1) \ z1)} is set
((w1 \ x1) \ x1) \ ((w1 \ x1) \ x1) is Element of the carrier of IT
the InternalDiff of IT . (((w1 \ x1) \ x1),((w1 \ x1) \ x1)) is Element of the carrier of IT
((x1 \ y1) \ z1) \ ((x1 \ z1) \ y1) is Element of the carrier of X
the InternalDiff of X . (((x1 \ y1) \ z1),((x1 \ z1) \ y1)) is Element of the carrier of X
Class (RI,(((x1 \ y1) \ z1) \ ((x1 \ z1) \ y1))) is Element of bool the carrier of X
{(((x1 \ y1) \ z1) \ ((x1 \ z1) \ y1))} is set
RI .: {(((x1 \ y1) \ z1) \ ((x1 \ z1) \ y1))} is set
w1 is Element of the carrier of IT
x1 is Element of the carrier of IT
w1 \ x1 is Element of the carrier of IT
the InternalDiff of IT . (w1,x1) is Element of the carrier of IT
x1 \ w1 is Element of the carrier of IT
the InternalDiff of IT . (x1,w1) is Element of the carrier of IT
x1 is set
Class (RI,x1) is Element of bool the carrier of X
{x1} is set
RI .: {x1} is set
y1 is set
Class (RI,y1) is Element of bool the carrier of X
{y1} is set
RI .: {y1} is set
y1 is Element of the carrier of X
x1 is Element of the carrier of X
y1 \ x1 is Element of the carrier of X
the InternalDiff of X . (y1,x1) is Element of the carrier of X
Class (RI,(y1 \ x1)) is Element of bool the carrier of X
{(y1 \ x1)} is set
RI .: {(y1 \ x1)} is set
[(y1 \ x1),(0. X)] is set
{(y1 \ x1),(0. X)} is set
{{(y1 \ x1),(0. X)},{(y1 \ x1)}} is set
(y1 \ x1) \ (0. X) is Element of the carrier of X
the InternalDiff of X . ((y1 \ x1),(0. X)) is Element of the carrier of X
x1 \ y1 is Element of the carrier of X
the InternalDiff of X . (x1,y1) is Element of the carrier of X
Class (RI,(x1 \ y1)) is Element of bool the carrier of X
{(x1 \ y1)} is set
RI .: {(x1 \ y1)} is set
[(x1 \ y1),(0. X)] is set
{(x1 \ y1),(0. X)} is set
{{(x1 \ y1),(0. X)},{(x1 \ y1)}} is set
(x1 \ y1) \ (0. X) is Element of the carrier of X
the InternalDiff of X . ((x1 \ y1),(0. X)) is Element of the carrier of X
[x1,y1] is set
{x1,y1} is set
{x1} is set
{{x1,y1},{x1}} is set
w1 is Element of the carrier of IT
x1 is set
Class (RI,x1) is Element of bool the carrier of X
{x1} is set
RI .: {x1} is set
w1 \ w1 is Element of the carrier of IT
the InternalDiff of IT . (w1,w1) is Element of the carrier of IT
x1 is Element of the carrier of X
x1 \ x1 is Element of the carrier of X
the InternalDiff of X . (x1,x1) is Element of the carrier of X
Class (RI,(x1 \ x1)) is Element of bool the carrier of X
{(x1 \ x1)} is set
RI .: {(x1 \ x1)} 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
I is non empty Ideal of X
RI is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X,I)
(X,RI) is non empty BCIStr_0
Class RI is non empty a_partition of the carrier of X
(X,RI) is Relation-like [:(Class RI),(Class RI):] -defined Class RI -valued Function-like V18([:(Class RI),(Class RI):], Class RI) Element of bool [:[:(Class RI),(Class RI):],(Class RI):]
[:(Class RI),(Class RI):] is non empty set
[:[:(Class RI),(Class RI):],(Class RI):] is non empty set
bool [:[:(Class RI),(Class RI):],(Class RI):] is non empty set
(X,RI) is Element of Class RI
bool the carrier of X is non empty set
0. X is V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
Class (RI,(0. X)) is Element of bool the carrier of X
{(0. X)} is set
RI .: {(0. X)} is set
BCIStr_0(# (Class RI),(X,RI),(X,RI) #) is strict BCIStr_0
X is non empty being_B being_C being_I being_BCI-4 BCIStr_0
BCK-part X is non empty Element of bool the carrier of X
the carrier of X is non empty set
bool the carrier of X is non empty set
0. X is V44(X) atom (X) (X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : 0. X <= b1 } is set
I is non empty Ideal of X
RI is Relation-like the carrier of X -defined the carrier of X -valued total reflexive symmetric transitive (X,I)
(X,RI) is non empty strict being_B being_C being_I being_BCI-4 BCIStr_0
Class RI is non empty a_partition of the carrier of X
(X,RI) is Relation-like [:(Class RI),(Class RI):] -defined Class RI -valued Function-like V18([:(Class RI),(Class RI):], Class RI) Element of bool [:[:(Class RI),(Class RI):],(Class RI):]
[:(Class RI),(Class RI):] is non empty set
[:[:(Class RI),(Class RI):],(Class RI):] is non empty set
bool [:[:(Class RI),(Class RI):],(Class RI):] is non empty set
(X,RI) is Element of Class RI
Class (RI,(0. X)) is Element of bool the carrier of X
{(0. X)} is set
RI .: {(0. X)} is set
BCIStr_0(# (Class RI),(X,RI),(X,RI) #) is strict BCIStr_0
the carrier of (X,RI) is non empty set
w1 is Element of the carrier of (X,RI)
w1 ` is Element of the carrier of (X,RI)
0. (X,RI) is V44((X,RI)) atom ((X,RI)) ((X,RI)) Element of the carrier of (X,RI)
the ZeroF of (X,RI) is Element of the carrier of (X,RI)
(0. (X,RI)) \ w1 is Element of the carrier of (X,RI)
the InternalDiff of (X,RI) is Relation-like [: the carrier of (X,RI), the carrier of (X,RI):] -defined the carrier of (X,RI) -valued Function-like V18([: the carrier of (X,RI), the carrier of (X,RI):], the carrier of (X,RI)) Element of bool [:[: the carrier of (X,RI), the carrier of (X,RI):], the carrier of (X,RI):]
[: the carrier of (X,RI), the carrier of (X,RI):] is non empty set
[:[: the carrier of (X,RI), the carrier of (X,RI):], the carrier of (X,RI):] is non empty set
bool [:[: the carrier of (X,RI), the carrier of (X,RI):], the carrier of (X,RI):] is non empty set
the InternalDiff of (X,RI) . ((0. (X,RI)),w1) is Element of the carrier of (X,RI)
(w1 `) ` is Element of the carrier of (X,RI)
(0. (X,RI)) \ (w1 `) is Element of the carrier of (X,RI)
the InternalDiff of (X,RI) . ((0. (X,RI)),(w1 `)) is Element of the carrier of (X,RI)
x1 is set
Class (RI,x1) is Element of bool the carrier of X
{x1} is set
RI .: {x1} is set
x1 is Element of the carrier of X
x1 ` is Element of the carrier of X
(0. X) \ x1 is Element of the carrier of X
the InternalDiff of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued 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 non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the InternalDiff of X . ((0. X),x1) is Element of the carrier of X
Class (RI,(x1 `)) is Element of bool the carrier of X
{(x1 `)} is set
RI .: {(x1 `)} is set
(x1 `) ` is Element of the carrier of X
(0. X) \ (x1 `) is Element of the carrier of X
the InternalDiff of X . ((0. X),(x1 `)) is Element of the carrier of X
Class (RI,((x1 `) `)) is Element of bool the carrier of X
{((x1 `) `)} is set
RI .: {((x1 `) `)} is set
x1 \ ((x1 `) `) is Element of the carrier of X
the InternalDiff of X . (x1,((x1 `) `)) is Element of the carrier of X
((x1 `) `) \ x1 is Element of the carrier of X
the InternalDiff of X . (((x1 `) `),x1) is Element of the carrier of X
[((x1 `) `),x1] is set
{((x1 `) `),x1} is set
{{((x1 `) `),x1},{((x1 `) `)}} is set