:: 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

( not b

{ b

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

( not b

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

( not b

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

( not b

(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

( b

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

( not b

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

( not b

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

( not b

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

( not b

(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

( not b

(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

( not b

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

( not b

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

( not b

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

( not b

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

( not b

(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

( not b

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

( not b

(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

( not b

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

( not b

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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

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

( not b

((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

U_FT c

U_FT B1 is Element of bool the carrier of n