:: FINTOPO3 semantic presentation

REAL is set
NAT is non empty V4() V5() V6() Element of bool REAL
bool REAL is non empty set
NAT is non empty V4() V5() V6() set
bool NAT is non empty set
{} is set
the empty V4() V5() V6() V8() V9() V10() set is empty V4() V5() V6() V8() V9() V10() set
1 is non empty V4() V5() V6() V10() Element of NAT
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
T ` is Element of bool the carrier of S
the carrier of S \ T is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of S : for b<sub>2</sub> being Element of the carrier of S holds
( not b<sub>2</sub> in T ` or not b₁ in U_FT b₂ ) } is set
{ b₁ where b₁ is Element of the carrier of S : S₁[b₁] } is set
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
T ^f is Element of bool the carrier of S
x is set
n is Element of the carrier of S
U_FT n is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T) is Element of bool the carrier of S
T ` is Element of bool the carrier of S
the carrier of S \ T is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of S : for b<sub>2</sub> being Element of the carrier of S holds
( not b<sub>2</sub> in T ` or not b₁ in U_FT b₂ ) } is set
x is Element of the carrier of S
n is Element of the carrier of S
U_FT n is Element of bool the carrier of S
k is Element of the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T) is Element of bool the carrier of S
T ` is Element of bool the carrier of S
the carrier of S \ T is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of S : for b<sub>2</sub> being Element of the carrier of S holds
( not b<sub>2</sub> in T ` or not b₁ in U_FT b₂ ) } is set
x is set
n is Element of the carrier of S
U_FT n is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T) is Element of bool the carrier of S
T ` is Element of bool the carrier of S
the carrier of S \ T is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of S : for b<sub>2</sub> being Element of the carrier of S holds
( not b<sub>2</sub> in T ` or not b₁ in U_FT b₂ ) } is set
(T `) ^f is Element of bool the carrier of S
((T `) ^f) ` is Element of bool the carrier of S
the carrier of S \ ((T `) ^f) is set
x is set
{ b₁ where b₁ is Element of the carrier of S : ex b₂ being Element of the carrier of S st
( b₂ in T ` & b<sub>1</sub> in U_FT b<sub>2</sub> ) } is set
n is Element of the carrier of S
k is Element of the carrier of S
U_FT k is Element of bool the carrier of S
n is Element of the carrier of S
U_FT n is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
T ^f is Element of bool the carrier of S
x is Element of bool the carrier of S
x ^f is Element of bool the carrier of S
n is set
k is Element of the carrier of S
U_FT k is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T) is Element of bool the carrier of S
T ` is Element of bool the carrier of S
the carrier of S \ T is set
{ b₁ where b₁ is Element of the carrier of S : for b₂ being Element of the carrier of S holds
( not b₂ in T ` or not b<sub>1</sub> in U_FT b<sub>2</sub> ) } is set
x is Element of bool the carrier of S
(S,x) is Element of bool the carrier of S
x ` is Element of bool the carrier of S
the carrier of S \ x is set
{ b₁ where b₁ is Element of the carrier of S : for b₂ being Element of the carrier of S holds
( not b₂ in x ` or not b<sub>1</sub> in U_FT b<sub>2</sub> ) } is set
n is set
k is Element of the carrier of S
U_FT k is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
T ^b is Element of bool the carrier of S
x is Element of bool the carrier of S
T /\ x is Element of bool the carrier of S
(T /\ x) ^b is Element of bool the carrier of S
x ^b is Element of bool the carrier of S
(T ^b) /\ (x ^b) is Element of bool the carrier of S
n is set
k is Element of the carrier of S
U_FT k is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
T ^b is Element of bool the carrier of S
x is Element of bool the carrier of S
T \/ x is Element of bool the carrier of S
(T \/ x) ^b is Element of bool the carrier of S
x ^b is Element of bool the carrier of S
(T ^b) \/ (x ^b) is Element of bool the carrier of S
n is set
k is Element of the carrier of S
U_FT k is Element of bool the carrier of S
n is set
k is Element of the carrier of S
U_FT k is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
T ^i is Element of bool the carrier of S
x is Element of bool the carrier of S
x ^i is Element of bool the carrier of S
(T ^i) \/ (x ^i) is Element of bool the carrier of S
T \/ x is Element of bool the carrier of S
(T \/ x) ^i is Element of bool the carrier of S
n is set
k is Element of the carrier of S
U_FT k is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
T ^i is Element of bool the carrier of S
x is Element of bool the carrier of S
x ^i is Element of bool the carrier of S
(T ^i) /\ (x ^i) is Element of bool the carrier of S
T /\ x is Element of bool the carrier of S
(T /\ x) ^i is Element of bool the carrier of S
n is set
k is Element of the carrier of S
U_FT k is Element of bool the carrier of S
n is set
k is Element of the carrier of S
U_FT k is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
T ^f is Element of bool the carrier of S
x is Element of bool the carrier of S
x ^f is Element of bool the carrier of S
(T ^f) \/ (x ^f) is Element of bool the carrier of S
T \/ x is Element of bool the carrier of S
(T \/ x) ^f is Element of bool the carrier of S
n is set
k is Element of the carrier of S
U_FT k is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T) is Element of bool the carrier of S
T ` is Element of bool the carrier of S
the carrier of S \ T is set
{ b₁ where b₁ is Element of the carrier of S : for b₂ being Element of the carrier of S holds
( not b₂ in T ` or not b<sub>1</sub> in U_FT b<sub>2</sub> ) } is set
x is Element of bool the carrier of S
(S,x) is Element of bool the carrier of S
x ` is Element of bool the carrier of S
the carrier of S \ x is set
{ b₁ where b₁ is Element of the carrier of S : for b₂ being Element of the carrier of S holds
( not b₂ in x ` or not b<sub>1</sub> in U_FT b<sub>2</sub> ) } is set
(S,T) /\ (S,x) is Element of bool the carrier of S
T /\ x is Element of bool the carrier of S
(S,(T /\ x)) is Element of bool the carrier of S
(T /\ x) ` is Element of bool the carrier of S
the carrier of S \ (T /\ x) is set
{ b₁ where b₁ is Element of the carrier of S : for b₂ being Element of the carrier of S holds
( not b₂ in (T /\ x) ` or not b<sub>1</sub> in U_FT b<sub>2</sub> ) } is set
(x `) ^f is Element of bool the carrier of S
((x `) ^f) ` is Element of bool the carrier of S
the carrier of S \ ((x `) ^f) is set
(T `) ^f is Element of bool the carrier of S
((T `) ^f) ` is Element of bool the carrier of S
the carrier of S \ ((T `) ^f) is set
(((T `) ^f) `) /\ (S,x) is Element of bool the carrier of S
((T `) ^f) \/ ((x `) ^f) is Element of bool the carrier of S
(((T `) ^f) \/ ((x `) ^f)) ` is Element of bool the carrier of S
the carrier of S \ (((T `) ^f) \/ ((x `) ^f)) is set
(T `) \/ (x `) is Element of bool the carrier of S
((T `) \/ (x `)) ^f is Element of bool the carrier of S
(((T `) \/ (x `)) ^f) ` is Element of bool the carrier of S
the carrier of S \ (((T `) \/ (x `)) ^f) is set
((T /\ x) `) ^f is Element of bool the carrier of S
(((T /\ x) `) ^f) ` is Element of bool the carrier of S
the carrier of S \ (((T /\ x) `) ^f) is set
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
0 is V4() V5() V6() V10() Element of NAT
T is Element of bool the carrier of S
x is V4() V5() V6() V10() Element of NAT
n is Element of bool the carrier of S
k is Element of bool the carrier of S
k ^b is Element of bool the carrier of S
B1 is Element of bool the carrier of S
B1 ^b is Element of bool the carrier of S
x is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
x . 0 is Element of bool the carrier of S
x is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
x . 0 is Element of bool the carrier of S
n is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
n . 0 is Element of bool the carrier of S
k is V4() V5() V6() V10() Element of NAT
x . k is Element of bool the carrier of S
n . k is Element of bool the carrier of S
k + 1 is V4() V5() V6() V10() Element of NAT
x . (k + 1) is Element of bool the carrier of S
n . (k + 1) is Element of bool the carrier of S
B1 is Element of bool the carrier of S
B1 ^b is Element of bool the carrier of S
dom x is set
dom n is set
k is set
x . k is set
n . k is set
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
x is V4() V5() V6() V10() set
(S,T) . x is set
n is V4() V5() V6() V10() Element of NAT
(S,T) . n is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
T is Element of bool the carrier of S
x is V4() V5() V6() V10() Element of NAT
n is Element of bool the carrier of S
k is Element of bool the carrier of S
k ^i is Element of bool the carrier of S
B1 is Element of bool the carrier of S
B1 ^i is Element of bool the carrier of S
x is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
x . 0 is Element of bool the carrier of S
x is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
x . 0 is Element of bool the carrier of S
n is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
n . 0 is Element of bool the carrier of S
k is V4() V5() V6() V10() Element of NAT
x . k is Element of bool the carrier of S
n . k is Element of bool the carrier of S
k + 1 is V4() V5() V6() V10() Element of NAT
x . (k + 1) is Element of bool the carrier of S
n . (k + 1) is Element of bool the carrier of S
B1 is Element of bool the carrier of S
B1 ^i is Element of bool the carrier of S
dom x is set
dom n is set
k is set
x . k is set
n . k is set
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
x is V4() V5() V6() V10() set
(S,T) . x is set
n is V4() V5() V6() V10() Element of NAT
(S,T) . n is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
x is V4() V5() V6() V10() Element of NAT
x + 1 is V4() V5() V6() V10() Element of NAT
(S,T,(x + 1)) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . (x + 1) is set
(S,T,x) is Element of bool the carrier of S
(S,T) . x is set
(S,T,x) ^b is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T,0) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . 0 is set
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T,1) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . 1 is set
T ^b is Element of bool the carrier of S
(S,T) . 0 is Element of bool the carrier of S
0 + 1 is V4() V5() V6() V10() Element of NAT
(S,T) . (0 + 1) is Element of bool the carrier of S
2 is non empty V4() V5() V6() V10() Element of NAT
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T,2) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . 2 is set
T ^b is Element of bool the carrier of S
(T ^b) ^b is Element of bool the carrier of S
(S,T) . 1 is Element of bool the carrier of S
1 + 1 is V4() V5() V6() V10() Element of NAT
(S,T) . (1 + 1) is Element of bool the carrier of S
x is Element of bool the carrier of S
x ^b is Element of bool the carrier of S
(S,T,1) is Element of bool the carrier of S
(S,T) . 1 is set
(S,T,1) ^b is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
x is Element of bool the carrier of S
T \/ x is Element of bool the carrier of S
n is V4() V5() V6() V10() Element of NAT
(S,(T \/ x),n) is Element of bool the carrier of S
(S,(T \/ x)) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,(T \/ x)) . n is set
(S,T,n) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
(S,T) . n is set
(S,x,n) is Element of bool the carrier of S
(S,x) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
(S,x) . n is set
(S,T,n) \/ (S,x,n) is Element of bool the carrier of S
k is V4() V5() V6() V10() Element of NAT
(S,(T \/ x)) . k is Element of bool the carrier of S
(S,T) . k is Element of bool the carrier of S
(S,x) . k is Element of bool the carrier of S
((S,T) . k) \/ ((S,x) . k) is Element of bool the carrier of S
k + 1 is V4() V5() V6() V10() Element of NAT
(S,(T \/ x)) . (k + 1) is Element of bool the carrier of S
(S,T) . (k + 1) is Element of bool the carrier of S
(S,x) . (k + 1) is Element of bool the carrier of S
((S,T) . (k + 1)) \/ ((S,x) . (k + 1)) is Element of bool the carrier of S
(S,(T \/ x),k) is Element of bool the carrier of S
(S,(T \/ x)) . k is set
(S,(T \/ x),k) ^b is Element of bool the carrier of S
(S,T,k) is Element of bool the carrier of S
(S,T) . k is set
(S,T,k) ^b is Element of bool the carrier of S
(S,x,k) is Element of bool the carrier of S
(S,x) . k is set
(S,x,k) ^b is Element of bool the carrier of S
((S,T,k) ^b) \/ ((S,x,k) ^b) is Element of bool the carrier of S
(S,T,(k + 1)) is Element of bool the carrier of S
(S,T) . (k + 1) is set
(S,T,(k + 1)) \/ ((S,x,k) ^b) is Element of bool the carrier of S
(S,(T \/ x)) . 0 is Element of bool the carrier of S
(S,T) . 0 is Element of bool the carrier of S
((S,T) . 0) \/ x is Element of bool the carrier of S
(S,x) . 0 is Element of bool the carrier of S
((S,T) . 0) \/ ((S,x) . 0) is Element of bool the carrier of S
k is V4() V5() V6() V10() Element of NAT
(S,(T \/ x)) . k is Element of bool the carrier of S
(S,T) . k is Element of bool the carrier of S
(S,x) . k is Element of bool the carrier of S
((S,T) . k) \/ ((S,x) . k) is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
x is V4() V5() V6() V10() Element of NAT
x + 1 is V4() V5() V6() V10() Element of NAT
(S,T,(x + 1)) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . (x + 1) is set
(S,T,x) is Element of bool the carrier of S
(S,T) . x is set
(S,T,x) ^i is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T,0) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . 0 is set
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T,1) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . 1 is set
T ^i is Element of bool the carrier of S
(S,T) . 0 is Element of bool the carrier of S
0 + 1 is V4() V5() V6() V10() Element of NAT
(S,T) . (0 + 1) is Element of bool the carrier of S
x is Element of bool the carrier of S
x ^i is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T,2) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . 2 is set
T ^i is Element of bool the carrier of S
(T ^i) ^i is Element of bool the carrier of S
1 + 1 is V4() V5() V6() V10() Element of NAT
(S,T,(1 + 1)) is Element of bool the carrier of S
(S,T) . (1 + 1) is set
(S,T,1) is Element of bool the carrier of S
(S,T) . 1 is set
(S,T,1) ^i is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
x is Element of bool the carrier of S
T /\ x is Element of bool the carrier of S
(S,(T /\ x)) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
(S,x) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
n is V4() V5() V6() V10() Element of NAT
(S,(T /\ x),n) is Element of bool the carrier of S
(S,(T /\ x)) . n is set
(S,T,n) is Element of bool the carrier of S
(S,T) . n is set
(S,x,n) is Element of bool the carrier of S
(S,x) . n is set
(S,T,n) /\ (S,x,n) is Element of bool the carrier of S
k is V4() V5() V6() V10() Element of NAT
(S,(T /\ x)) . k is Element of bool the carrier of S
(S,T) . k is Element of bool the carrier of S
(S,x) . k is Element of bool the carrier of S
((S,T) . k) /\ ((S,x) . k) is Element of bool the carrier of S
k + 1 is V4() V5() V6() V10() Element of NAT
(S,(T /\ x)) . (k + 1) is Element of bool the carrier of S
(S,T) . (k + 1) is Element of bool the carrier of S
(S,x) . (k + 1) is Element of bool the carrier of S
((S,T) . (k + 1)) /\ ((S,x) . (k + 1)) is Element of bool the carrier of S
(S,(T /\ x),k) is Element of bool the carrier of S
(S,(T /\ x)) . k is set
(S,(T /\ x),k) ^i is Element of bool the carrier of S
(S,T,k) is Element of bool the carrier of S
(S,T) . k is set
(S,T,k) ^i is Element of bool the carrier of S
(S,x,k) is Element of bool the carrier of S
(S,x) . k is set
(S,x,k) ^i is Element of bool the carrier of S
((S,T,k) ^i) /\ ((S,x,k) ^i) is Element of bool the carrier of S
(S,T,(k + 1)) is Element of bool the carrier of S
(S,T) . (k + 1) is set
(S,T,(k + 1)) /\ ((S,x,k) ^i) is Element of bool the carrier of S
(S,(T /\ x)) . 0 is Element of bool the carrier of S
(S,T) . 0 is Element of bool the carrier of S
((S,T) . 0) /\ x is Element of bool the carrier of S
(S,x) . 0 is Element of bool the carrier of S
((S,T) . 0) /\ ((S,x) . 0) is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
x is V4() V5() V6() V10() Element of NAT
(S,T) . x is Element of bool the carrier of S
x + 1 is V4() V5() V6() V10() Element of NAT
(S,T) . (x + 1) is Element of bool the carrier of S
T ^b is Element of bool the carrier of S
(S,T,x) is Element of bool the carrier of S
(S,T) . x is set
(S,T,x) ^b is Element of bool the carrier of S
(S,T,(x + 1)) is Element of bool the carrier of S
(S,T) . (x + 1) is set
x is V4() V5() V6() V10() Element of NAT
(S,T,x) is Element of bool the carrier of S
(S,T) . x is set
(S,T) . 0 is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
x is V4() V5() V6() V10() Element of NAT
(S,T) . x is Element of bool the carrier of S
x + 1 is V4() V5() V6() V10() Element of NAT
(S,T) . (x + 1) is Element of bool the carrier of S
(S,T,x) is Element of bool the carrier of S
(S,T) . x is set
(S,T,x) ^i is Element of bool the carrier of S
T ^i is Element of bool the carrier of S
(S,T,(x + 1)) is Element of bool the carrier of S
(S,T) . (x + 1) is set
x is V4() V5() V6() V10() Element of NAT
(S,T,x) is Element of bool the carrier of S
(S,T) . x is set
(S,T) . 0 is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
x is V4() V5() V6() V10() Element of NAT
(S,T,x) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . x is set
x + 1 is V4() V5() V6() V10() Element of NAT
(S,T,(x + 1)) is Element of bool the carrier of S
(S,T) . (x + 1) is set
(S,T) . x is Element of bool the carrier of S
((S,T) . x) ^b is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
x is V4() V5() V6() V10() Element of NAT
x + 1 is V4() V5() V6() V10() Element of NAT
(S,T,(x + 1)) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . (x + 1) is set
(S,T,x) is Element of bool the carrier of S
(S,T) . x is set
(S,T) . x is Element of bool the carrier of S
((S,T) . x) ^i is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
T ` is Element of bool the carrier of S
the carrier of S \ T is set
x is V4() V5() V6() V10() Element of NAT
(S,(T `),x) is Element of bool the carrier of S
(S,(T `)) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,(T `)) . x is set
(S,(T `),x) ` is Element of bool the carrier of S
the carrier of S \ (S,(T `),x) is set
(S,T,x) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
(S,T) . x is set
x + 1 is V4() V5() V6() V10() Element of NAT
(S,(T `),(x + 1)) is Element of bool the carrier of S
(S,(T `)) . (x + 1) is set
(S,(T `),(x + 1)) ` is Element of bool the carrier of S
the carrier of S \ (S,(T `),(x + 1)) is set
(S,T,(x + 1)) is Element of bool the carrier of S
(S,T) . (x + 1) is set
(S,T,x) ^b is Element of bool the carrier of S
((S,(T `),x) `) ` is Element of bool the carrier of S
the carrier of S \ ((S,(T `),x) `) is set
(((S,(T `),x) `) `) ^i is Element of bool the carrier of S
((((S,(T `),x) `) `) ^i) ` is Element of bool the carrier of S
the carrier of S \ ((((S,(T `),x) `) `) ^i) is set
(S,(T `),0) is Element of bool the carrier of S
(S,(T `)) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,(T `)) . 0 is set
(S,(T `),0) ` is Element of bool the carrier of S
the carrier of S \ (S,(T `),0) is set
(T `) ` is Element of bool the carrier of S
the carrier of S \ (T `) is set
(S,T,0) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
(S,T) . 0 is set
x is V4() V5() V6() V10() Element of NAT
(S,(T `),x) is Element of bool the carrier of S
(S,(T `)) . x is set
(S,(T `),x) ` is Element of bool the carrier of S
the carrier of S \ (S,(T `),x) is set
(S,T,x) is Element of bool the carrier of S
(S,T) . x is set
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
T ` is Element of bool the carrier of S
the carrier of S \ T is set
x is V4() V5() V6() V10() Element of NAT
(S,(T `),x) is Element of bool the carrier of S
(S,(T `)) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,(T `)) . x is set
(S,(T `),x) ` is Element of bool the carrier of S
the carrier of S \ (S,(T `),x) is set
(S,T,x) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
(S,T) . x is set
(T `) ` is Element of bool the carrier of S
the carrier of S \ (T `) is set
(S,((T `) `),x) is Element of bool the carrier of S
(S,((T `) `)) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
(S,((T `) `)) . x is set
(S,((T `) `),x) ` is Element of bool the carrier of S
the carrier of S \ (S,((T `) `),x) is set
((S,((T `) `),x) `) ` is Element of bool the carrier of S
the carrier of S \ ((S,((T `) `),x) `) is set
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
x is Element of bool the carrier of S
T \/ x is Element of bool the carrier of S
(T \/ x) ` is Element of bool the carrier of S
the carrier of S \ (T \/ x) is set
n is V4() V5() V6() V10() Element of NAT
(S,T,n) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . n is set
(S,x,n) is Element of bool the carrier of S
(S,x) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
(S,x) . n is set
(S,T,n) \/ (S,x,n) is Element of bool the carrier of S
(S,((T \/ x) `),n) is Element of bool the carrier of S
(S,((T \/ x) `)) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
(S,((T \/ x) `)) . n is set
(S,((T \/ x) `),n) ` is Element of bool the carrier of S
the carrier of S \ (S,((T \/ x) `),n) is set
(S,(T \/ x),n) is Element of bool the carrier of S
(S,(T \/ x)) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
(S,(T \/ x)) . n is set
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
x is Element of bool the carrier of S
T /\ x is Element of bool the carrier of S
(T /\ x) ` is Element of bool the carrier of S
the carrier of S \ (T /\ x) is set
n is V4() V5() V6() V10() Element of NAT
(S,T,n) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . n is set
(S,x,n) is Element of bool the carrier of S
(S,x) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
(S,x) . n is set
(S,T,n) /\ (S,x,n) is Element of bool the carrier of S
(S,((T /\ x) `),n) is Element of bool the carrier of S
(S,((T /\ x) `)) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
(S,((T /\ x) `)) . n is set
(S,((T /\ x) `),n) ` is Element of bool the carrier of S
the carrier of S \ (S,((T /\ x) `),n) is set
(S,(T /\ x),n) is Element of bool the carrier of S
(S,(T /\ x)) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
(S,(T /\ x)) . n is set
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
T is Element of bool the carrier of S
x is V4() V5() V6() V10() Element of NAT
n is Element of bool the carrier of S
k is Element of bool the carrier of S
k ^f is Element of bool the carrier of S
B1 is Element of bool the carrier of S
B1 ^f is Element of bool the carrier of S
x is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
x . 0 is Element of bool the carrier of S
x is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
x . 0 is Element of bool the carrier of S
n is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
n . 0 is Element of bool the carrier of S
dom x is set
dom n is set
k is V4() V5() V6() V10() Element of NAT
x . k is Element of bool the carrier of S
n . k is Element of bool the carrier of S
B1 is V4() V5() V6() V10() Element of NAT
x . B1 is Element of bool the carrier of S
n . B1 is Element of bool the carrier of S
B1 + 1 is V4() V5() V6() V10() Element of NAT
x . (B1 + 1) is Element of bool the carrier of S
n . (B1 + 1) is Element of bool the carrier of S
B1 is Element of bool the carrier of S
B1 ^f is Element of bool the carrier of S
k is set
x . k is set
n . k is set
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
x is V4() V5() V6() V10() set
(S,T) . x is set
n is V4() V5() V6() V10() Element of NAT
(S,T) . n is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
T is Element of bool the carrier of S
x is V4() V5() V6() V10() Element of NAT
n is Element of bool the carrier of S
(S,n) is Element of bool the carrier of S
n ` is Element of bool the carrier of S
the carrier of S \ n is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of S : for b<sub>2</sub> being Element of the carrier of S holds
( not b<sub>2</sub> in n ` or not b₁ in U_FT b₂ ) } is set
k is Element of bool the carrier of S
(S,k) is Element of bool the carrier of S
k ` is Element of bool the carrier of S
the carrier of S \ k is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of S : for b<sub>2</sub> being Element of the carrier of S holds
( not b<sub>2</sub> in k ` or not b₁ in U_FT b₂ ) } is set
x is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
x . 0 is Element of bool the carrier of S
x is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
x . 0 is Element of bool the carrier of S
n is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
n . 0 is Element of bool the carrier of S
k is V4() V5() V6() V10() Element of NAT
x . k is Element of bool the carrier of S
n . k is Element of bool the carrier of S
k + 1 is V4() V5() V6() V10() Element of NAT
x . (k + 1) is Element of bool the carrier of S
n . (k + 1) is Element of bool the carrier of S
B1 is Element of bool the carrier of S
(S,B1) is Element of bool the carrier of S
B1 ` is Element of bool the carrier of S
the carrier of S \ B1 is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of S : for b<sub>2</sub> being Element of the carrier of S holds
( not b<sub>2</sub> in B1 ` or not b₁ in U_FT b₂ ) } is set
dom x is set
dom n is set
k is set
x . k is set
n . k is set
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
x is V4() V5() V6() V10() set
(S,T) . x is set
n is V4() V5() V6() V10() Element of NAT
(S,T) . n is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
x is V4() V5() V6() V10() Element of NAT
x + 1 is V4() V5() V6() V10() Element of NAT
(S,T,(x + 1)) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . (x + 1) is set
(S,T,x) is Element of bool the carrier of S
(S,T) . x is set
(S,T,x) ^f is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T,0) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . 0 is set
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T,1) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . 1 is set
T ^f is Element of bool the carrier of S
(S,T) . 0 is Element of bool the carrier of S
0 + 1 is V4() V5() V6() V10() Element of NAT
(S,T) . (0 + 1) is Element of bool the carrier of S
x is Element of bool the carrier of S
x ^f is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T,2) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . 2 is set
T ^f is Element of bool the carrier of S
(T ^f) ^f is Element of bool the carrier of S
1 + 1 is V4() V5() V6() V10() Element of NAT
(S,T,(1 + 1)) is Element of bool the carrier of S
(S,T) . (1 + 1) is set
(S,T,1) is Element of bool the carrier of S
(S,T) . 1 is set
(S,T,1) ^f is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
x is Element of bool the carrier of S
T \/ x is Element of bool the carrier of S
(S,(T \/ x)) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
(S,x) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
n is V4() V5() V6() V10() Element of NAT
(S,(T \/ x),n) is Element of bool the carrier of S
(S,(T \/ x)) . n is set
(S,T,n) is Element of bool the carrier of S
(S,T) . n is set
(S,x,n) is Element of bool the carrier of S
(S,x) . n is set
(S,T,n) \/ (S,x,n) is Element of bool the carrier of S
k is V4() V5() V6() V10() Element of NAT
(S,(T \/ x)) . k is Element of bool the carrier of S
(S,T) . k is Element of bool the carrier of S
(S,x) . k is Element of bool the carrier of S
((S,T) . k) \/ ((S,x) . k) is Element of bool the carrier of S
k + 1 is V4() V5() V6() V10() Element of NAT
(S,(T \/ x)) . (k + 1) is Element of bool the carrier of S
(S,T) . (k + 1) is Element of bool the carrier of S
(S,x) . (k + 1) is Element of bool the carrier of S
((S,T) . (k + 1)) \/ ((S,x) . (k + 1)) is Element of bool the carrier of S
(S,(T \/ x),k) is Element of bool the carrier of S
(S,(T \/ x)) . k is set
(S,(T \/ x),k) ^f is Element of bool the carrier of S
(S,T,k) is Element of bool the carrier of S
(S,T) . k is set
(S,T,k) ^f is Element of bool the carrier of S
(S,x,k) is Element of bool the carrier of S
(S,x) . k is set
(S,x,k) ^f is Element of bool the carrier of S
((S,T,k) ^f) \/ ((S,x,k) ^f) is Element of bool the carrier of S
(S,T,(k + 1)) is Element of bool the carrier of S
(S,T) . (k + 1) is set
(S,T,(k + 1)) \/ ((S,x,k) ^f) is Element of bool the carrier of S
(S,(T \/ x)) . 0 is Element of bool the carrier of S
(S,T) . 0 is Element of bool the carrier of S
((S,T) . 0) \/ x is Element of bool the carrier of S
(S,x) . 0 is Element of bool the carrier of S
((S,T) . 0) \/ ((S,x) . 0) is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
x is V4() V5() V6() V10() Element of NAT
(S,T) . x is Element of bool the carrier of S
x + 1 is V4() V5() V6() V10() Element of NAT
(S,T) . (x + 1) is Element of bool the carrier of S
T ^f is Element of bool the carrier of S
(S,T,x) is Element of bool the carrier of S
(S,T) . x is set
(S,T,x) ^f is Element of bool the carrier of S
(S,T,(x + 1)) is Element of bool the carrier of S
(S,T) . (x + 1) is set
x is V4() V5() V6() V10() Element of NAT
(S,T,x) is Element of bool the carrier of S
(S,T) . x is set
(S,T) . 0 is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
x is V4() V5() V6() V10() Element of NAT
(S,T,x) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . x is set
x + 1 is V4() V5() V6() V10() Element of NAT
(S,T,(x + 1)) is Element of bool the carrier of S
(S,T) . (x + 1) is set
(S,T) . x is Element of bool the carrier of S
((S,T) . x) ^f is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
x is V4() V5() V6() V10() Element of NAT
x + 1 is V4() V5() V6() V10() Element of NAT
(S,T,(x + 1)) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . (x + 1) is set
(S,T,x) is Element of bool the carrier of S
(S,T) . x is set
(S,(S,T,x)) is Element of bool the carrier of S
(S,T,x) ` is Element of bool the carrier of S
the carrier of S \ (S,T,x) is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of S : for b<sub>2</sub> being Element of the carrier of S holds
( not b<sub>2</sub> in (S,T,x) ` or not b₁ in U_FT b₂ ) } is set
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T,0) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . 0 is set
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T,1) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . 1 is set
(S,T) is Element of bool the carrier of S
T ` is Element of bool the carrier of S
the carrier of S \ T is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of S : for b<sub>2</sub> being Element of the carrier of S holds
( not b<sub>2</sub> in T ` or not b₁ in U_FT b₂ ) } is set
(S,T) . 0 is Element of bool the carrier of S
0 + 1 is V4() V5() V6() V10() Element of NAT
(S,T) . (0 + 1) is Element of bool the carrier of S
x is Element of bool the carrier of S
(S,x) is Element of bool the carrier of S
x ` is Element of bool the carrier of S
the carrier of S \ x is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of S : for b<sub>2</sub> being Element of the carrier of S holds
( not b<sub>2</sub> in x ` or not b₁ in U_FT b₂ ) } is set
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T,2) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . 2 is set
(S,T) is Element of bool the carrier of S
T ` is Element of bool the carrier of S
the carrier of S \ T is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of S : for b<sub>2</sub> being Element of the carrier of S holds
( not b<sub>2</sub> in T ` or not b₁ in U_FT b₂ ) } is set
(S,(S,T)) is Element of bool the carrier of S
(S,T) ` is Element of bool the carrier of S
the carrier of S \ (S,T) is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of S : for b<sub>2</sub> being Element of the carrier of S holds
( not b<sub>2</sub> in (S,T) ` or not b₁ in U_FT b₂ ) } is set
1 + 1 is V4() V5() V6() V10() Element of NAT
(S,T,(1 + 1)) is Element of bool the carrier of S
(S,T) . (1 + 1) is set
(S,T,1) is Element of bool the carrier of S
(S,T) . 1 is set
(S,(S,T,1)) is Element of bool the carrier of S
(S,T,1) ` is Element of bool the carrier of S
the carrier of S \ (S,T,1) is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of S : for b<sub>2</sub> being Element of the carrier of S holds
( not b<sub>2</sub> in (S,T,1) ` or not b₁ in U_FT b₂ ) } is set
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
x is Element of bool the carrier of S
T /\ x is Element of bool the carrier of S
(S,(T /\ x)) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
(S,x) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
n is V4() V5() V6() V10() Element of NAT
(S,(T /\ x),n) is Element of bool the carrier of S
(S,(T /\ x)) . n is set
(S,T,n) is Element of bool the carrier of S
(S,T) . n is set
(S,x,n) is Element of bool the carrier of S
(S,x) . n is set
(S,T,n) /\ (S,x,n) is Element of bool the carrier of S
k is V4() V5() V6() V10() Element of NAT
(S,(T /\ x)) . k is Element of bool the carrier of S
(S,T) . k is Element of bool the carrier of S
(S,x) . k is Element of bool the carrier of S
((S,T) . k) /\ ((S,x) . k) is Element of bool the carrier of S
k + 1 is V4() V5() V6() V10() Element of NAT
(S,(T /\ x)) . (k + 1) is Element of bool the carrier of S
(S,T) . (k + 1) is Element of bool the carrier of S
(S,x) . (k + 1) is Element of bool the carrier of S
((S,T) . (k + 1)) /\ ((S,x) . (k + 1)) is Element of bool the carrier of S
(S,(T /\ x),k) is Element of bool the carrier of S
(S,(T /\ x)) . k is set
(S,(S,(T /\ x),k)) is Element of bool the carrier of S
(S,(T /\ x),k) ` is Element of bool the carrier of S
the carrier of S \ (S,(T /\ x),k) is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of S : for b<sub>2</sub> being Element of the carrier of S holds
( not b<sub>2</sub> in (S,(T /\ x),k) ` or not b₁ in U_FT b₂ ) } is set
(S,T,k) is Element of bool the carrier of S
(S,T) . k is set
(S,(S,T,k)) is Element of bool the carrier of S
(S,T,k) ` is Element of bool the carrier of S
the carrier of S \ (S,T,k) is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of S : for b<sub>2</sub> being Element of the carrier of S holds
( not b<sub>2</sub> in (S,T,k) ` or not b₁ in U_FT b₂ ) } is set
(S,x,k) is Element of bool the carrier of S
(S,x) . k is set
(S,(S,x,k)) is Element of bool the carrier of S
(S,x,k) ` is Element of bool the carrier of S
the carrier of S \ (S,x,k) is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of S : for b<sub>2</sub> being Element of the carrier of S holds
( not b<sub>2</sub> in (S,x,k) ` or not b₁ in U_FT b₂ ) } is set
(S,(S,T,k)) /\ (S,(S,x,k)) is Element of bool the carrier of S
(S,T,(k + 1)) is Element of bool the carrier of S
(S,T) . (k + 1) is set
(S,T,(k + 1)) /\ (S,(S,x,k)) is Element of bool the carrier of S
(S,(T /\ x)) . 0 is Element of bool the carrier of S
(S,T) . 0 is Element of bool the carrier of S
((S,T) . 0) /\ x is Element of bool the carrier of S
(S,x) . 0 is Element of bool the carrier of S
((S,T) . 0) /\ ((S,x) . 0) is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
x is V4() V5() V6() V10() Element of NAT
(S,T) . x is Element of bool the carrier of S
x + 1 is V4() V5() V6() V10() Element of NAT
(S,T) . (x + 1) is Element of bool the carrier of S
(S,T,x) is Element of bool the carrier of S
(S,T) . x is set
(S,(S,T,x)) is Element of bool the carrier of S
(S,T,x) ` is Element of bool the carrier of S
the carrier of S \ (S,T,x) is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of S : for b<sub>2</sub> being Element of the carrier of S holds
( not b<sub>2</sub> in (S,T,x) ` or not b₁ in U_FT b₂ ) } is set
(S,T) is Element of bool the carrier of S
T ` is Element of bool the carrier of S
the carrier of S \ T is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of S : for b<sub>2</sub> being Element of the carrier of S holds
( not b<sub>2</sub> in T ` or not b₁ in U_FT b₂ ) } is set
(S,T,(x + 1)) is Element of bool the carrier of S
(S,T) . (x + 1) is set
x is V4() V5() V6() V10() Element of NAT
(S,T,x) is Element of bool the carrier of S
(S,T) . x is set
(S,T) . 0 is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
x is V4() V5() V6() V10() Element of NAT
x + 1 is V4() V5() V6() V10() Element of NAT
(S,T,(x + 1)) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . (x + 1) is set
(S,T,x) is Element of bool the carrier of S
(S,T) . x is set
(S,T) . x is Element of bool the carrier of S
(S,((S,T) . x)) is Element of bool the carrier of S
((S,T) . x) ` is Element of bool the carrier of S
the carrier of S \ ((S,T) . x) is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of S : for b<sub>2</sub> being Element of the carrier of S holds
( not b<sub>2</sub> in ((S,T) . x) ` or not b₁ in U_FT b₂ ) } is set
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
T ` is Element of bool the carrier of S
the carrier of S \ T is set
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,(T `)) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
x is V4() V5() V6() V10() Element of NAT
(S,T,x) is Element of bool the carrier of S
(S,T) . x is set
(S,(T `),x) is Element of bool the carrier of S
(S,(T `)) . x is set
(S,(T `),x) ` is Element of bool the carrier of S
the carrier of S \ (S,(T `),x) is set
n is V4() V5() V6() V10() Element of NAT
(S,T) . n is Element of bool the carrier of S
(S,(T `)) . n is Element of bool the carrier of S
((S,(T `)) . n) ` is Element of bool the carrier of S
the carrier of S \ ((S,(T `)) . n) is set
n + 1 is V4() V5() V6() V10() Element of NAT
(S,T) . (n + 1) is Element of bool the carrier of S
(S,(T `)) . (n + 1) is Element of bool the carrier of S
((S,(T `)) . (n + 1)) ` is Element of bool the carrier of S
the carrier of S \ ((S,(T `)) . (n + 1)) is set
(S,T,n) is Element of bool the carrier of S
(S,T) . n is set
(S,(S,T,n)) is Element of bool the carrier of S
(S,T,n) ` is Element of bool the carrier of S
the carrier of S \ (S,T,n) is set
{ b₁ where b₁ is Element of the carrier of S : for b₂ being Element of the carrier of S holds
( not b₂ in (S,T,n) ` or not b<sub>1</sub> in U_FT b<sub>2</sub> ) } is set
((S,T) . n) ` is Element of bool the carrier of S
the carrier of S \ ((S,T) . n) is set
(((S,T) . n) `) ^f is Element of bool the carrier of S
((((S,T) . n) `) ^f) ` is Element of bool the carrier of S
the carrier of S \ ((((S,T) . n) `) ^f) is set
(S,(T `)) . 0 is Element of bool the carrier of S
((S,(T `)) . 0) ` is Element of bool the carrier of S
the carrier of S \ ((S,(T `)) . 0) is set
(T `) ` is Element of bool the carrier of S
the carrier of S \ (T `) is set
(S,T) . 0 is Element of bool the carrier of S
S is non empty RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is Element of bool the carrier of S
x is Element of bool the carrier of S
T /\ x is Element of bool the carrier of S
(T /\ x) ` is Element of bool the carrier of S
the carrier of S \ (T /\ x) is set
n is V4() V5() V6() V10() Element of NAT
(S,T,n) is Element of bool the carrier of S
(S,T) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,T) . n is set
(S,x,n) is Element of bool the carrier of S
(S,x) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
(S,x) . n is set
(S,T,n) /\ (S,x,n) is Element of bool the carrier of S
(S,((T /\ x) `),n) is Element of bool the carrier of S
(S,((T /\ x) `)) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
(S,((T /\ x) `)) . n is set
(S,((T /\ x) `),n) ` is Element of bool the carrier of S
the carrier of S \ (S,((T /\ x) `),n) is set
(S,(T /\ x),n) is Element of bool the carrier of S
(S,(T /\ x)) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
(S,(T /\ x)) . n is set
S is non empty RelStr
the carrier of S is non empty set
x is Element of the carrier of S
U_FT x is Element of bool the carrier of S
bool the carrier of S is non empty set
T is V4() V5() V6() V10() set
(S,(U_FT x),T) is Element of bool the carrier of S
(S,(U_FT x)) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,(U_FT x)) . T is set
S is non empty RelStr
the carrier of S is non empty set
T is Element of the carrier of S
(S,0,T) is Element of bool the carrier of S
bool the carrier of S is non empty set
U_FT T is Element of bool the carrier of S
(S,(U_FT T),0) is Element of bool the carrier of S
(S,(U_FT T)) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,(U_FT T)) . 0 is set
S is non empty RelStr
the carrier of S is non empty set
x is V4() V5() V6() V10() Element of NAT
x + 1 is V4() V5() V6() V10() Element of NAT
T is Element of the carrier of S
(S,(x + 1),T) is Element of bool the carrier of S
bool the carrier of S is non empty set
U_FT T is Element of bool the carrier of S
(S,(U_FT T),(x + 1)) is Element of bool the carrier of S
(S,(U_FT T)) is Relation-like NAT -defined bool the carrier of S -valued Function-like V29( NAT , bool the carrier of S) Element of bool [:NAT,(bool the carrier of S):]
[:NAT,(bool the carrier of S):] is non empty set
bool [:NAT,(bool the carrier of S):] is non empty set
(S,(U_FT T)) . (x + 1) is set
(S,x,T) is Element of bool the carrier of S
(S,(U_FT T),x) is Element of bool the carrier of S
(S,(U_FT T)) . x is set
(S,x,T) ^f is Element of bool the carrier of S
n is non empty RelStr
the carrier of n is non empty set
x is non empty RelStr
the carrier of x is non empty set
B1 is Element of the carrier of x
k is Element of the carrier of n
U_FT k is Element of bool the carrier of n
bool the carrier of n is non empty set
U_FT B1 is Element of bool the carrier of x
bool the carrier of x is non empty set
B1 is Element of the carrier of n
c₈ is Element of the carrier of x
U_FT c₈ is Element of bool the carrier of x
U_FT B1 is Element of bool the carrier of n