:: SUBLEMMA semantic presentation

REAL is V45() V46() V47() V51() V63() V64() V66() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V52() V61() V63() cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
COMPLEX is V45() V51() set
RAT is V45() V46() V47() V48() V51() set
INT is V45() V46() V47() V48() V49() V51() set
omega is non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V52() V61() V63() cardinal limit_cardinal set
bool omega is non empty V52() set
bool NAT is non empty V52() set

bool is non empty set

bool is non empty set
K370() is set

1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
TRUE is Element of K370()

[0,0] is V1() set
{0,0} is non empty functional V45() V46() V47() V48() V49() V50() V61() V63() set
is non empty trivial functional V45() V46() V47() V48() V49() V50() V61() V63() 1 -element set
is non empty set

is non empty Relation-like V52() set
is non empty Relation-like V52() set
bool is non empty V52() set
[0,0] is V1() Element of

[1,0] is V1() Element of
{1,0} is non empty V45() V46() V47() V48() V49() V50() V61() V63() set
{1} is non empty trivial V45() V46() V47() V48() V49() V50() V61() V63() 1 -element set
{{1,0},{1}} is non empty set

2 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
[2,0] is V1() Element of
{2,0} is non empty V45() V46() V47() V48() V49() V50() V61() V63() set
{2} is non empty trivial V45() V46() V47() V48() V49() V50() V61() V63() 1 -element set
{{2,0},{2}} is non empty set

3 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal Element of NAT
[3,0] is V1() Element of
{3,0} is non empty V45() V46() V47() V48() V49() V50() V61() V63() set
{3} is non empty trivial V45() V46() V47() V48() V49() V50() V61() V63() 1 -element set
{{3,0},{3}} is non empty set

proj1 xSQ is set

proj1 J is set

proj1 S is set

(Al +* A) +* J is Relation-like Function-like set

(Al +* xSQ) +* (A +* S) is Relation-like Function-like set
((Al +* xSQ) +* (A +* S)) +* J is Relation-like Function-like set
proj1 (Al +* xSQ) is set
proj1 Al is set
(proj1 Al) \/ (proj1 xSQ) is set
proj1 (A +* S) is set
proj1 A is set
() \/ () is set
proj1 ((Al +* xSQ) +* (A +* S)) is set
((proj1 Al) \/ (proj1 xSQ)) \/ (() \/ ()) is set
proj1 (((Al +* xSQ) +* (A +* S)) +* J) is set
(((proj1 Al) \/ (proj1 xSQ)) \/ (() \/ ())) \/ () is set
(() \/ ()) \/ () is set
((proj1 Al) \/ (proj1 xSQ)) \/ ((() \/ ()) \/ ()) is set
() \/ () is set
() \/ (() \/ ()) is set
((proj1 Al) \/ (proj1 xSQ)) \/ (() \/ (() \/ ())) is set
() \/ () is set
((proj1 Al) \/ (proj1 xSQ)) \/ (() \/ ()) is set
((proj1 Al) \/ (proj1 xSQ)) \/ () is set
(((proj1 Al) \/ (proj1 xSQ)) \/ ()) \/ () is set
(proj1 xSQ) \/ () is set
(proj1 Al) \/ ((proj1 xSQ) \/ ()) is set
((proj1 Al) \/ ((proj1 xSQ) \/ ())) \/ () is set
(proj1 Al) \/ () is set
((proj1 Al) \/ ()) \/ () is set
proj1 ((Al +* A) +* J) is set
xSQ is set
((Al +* A) +* J) . xSQ is set
(((Al +* xSQ) +* (A +* S)) +* J) . xSQ is set
((Al +* xSQ) +* (A +* S)) . xSQ is set
(Al +* A) . xSQ is set
(A +* S) . xSQ is set
A . xSQ is set
(Al +* xSQ) . xSQ is set
Al . xSQ is set
J . xSQ is set
proj1 (Al +* A) is set
(proj1 Al) \/ () is set
((proj1 Al) \/ ()) \/ () is set
Al is non empty Relation-like QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool ()
bool () is non empty set
A is Element of bound_QC-variables Al
{A} is non empty trivial 1 -element Element of bool ()
bool () is non empty set

proj1 J is set
() \ {A} is Element of bool ()
bool () is non empty set
J | (() \ {A}) is Relation-like Function-like set
J . A is set

{A} is non empty trivial 1 -element set
{A} --> (J . A) is non empty Relation-like {A} -defined {(J . A)} -valued Function-like constant total quasi_total Element of bool [:{A},{(J . A)}:]
{(J . A)} is non empty trivial 1 -element set
[:{A},{(J . A)}:] is non empty Relation-like set
bool [:{A},{(J . A)}:] is non empty set
(J | (() \ {A})) +* (A .--> (J . A)) is Relation-like Function-like set
(() \ {A}) \/ {A} is non empty set
() \/ {A} is non empty set
Al is non empty Relation-like QC-alphabet
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
A is non empty set
Valuations_in (Al,A) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
[:(),A:] is non empty Relation-like set
bool [:(),A:] is non empty set
Al is non empty Relation-like QC-alphabet
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
A is non empty set
Valuations_in (Al,A) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
[:(),A:] is non empty Relation-like set
bool [:(),A:] is non empty set

Funcs ((),A) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,A

dom (J +* xSQ) is Element of bool ()
bool () is non empty set
dom xSQ is Element of bool ()
() \/ (dom xSQ) is non empty set

proj1 S is set
proj2 S is set
rng (J +* xSQ) is Element of bool A
bool A is non empty set
rng J is Element of bool A
rng xSQ is Element of bool A
(rng J) \/ (rng xSQ) is Element of bool A
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
A is Element of CQC-Sub-WFF Al
A `1 is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
{ b1 where b1 is Element of QC-Sub-WFF Al : b1 `1 is Element of CQC-WFF Al } is set
J is Element of QC-Sub-WFF Al
J `1 is Element of QC-WFF Al
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
J is non empty set
Valuations_in (Al,J) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,J
A is Element of CQC-Sub-WFF Al

vSUB Al is non empty functional set

[:(),():] is non empty Relation-like set
bool [:(),():] is non empty set

(@ (A `2)) * xSQ is Relation-like bound_QC-variables Al -defined J -valued Function-like Element of bool [:(),J:]
[:(),J:] is non empty Relation-like set
bool [:(),J:] is non empty set
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
VERUM Al is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
A is Element of CQC-Sub-WFF Al
CQC_Sub A is Element of CQC-WFF Al
[:(),(QC-WFF Al):] is non empty Relation-like set
bool [:(),(QC-WFF Al):] is non empty set

J . A is Element of QC-WFF Al
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
J is non empty set
Valuations_in (Al,J) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,J
QC-pred_symbols Al is non empty set
K367(J) is set
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
A is non empty set
K367(A) is set
Valuations_in (Al,A) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,A

xSQ is Element of CQC-Sub-WFF Al
CQC_Sub xSQ is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set

(Al,xSQ,A,S) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
[:(),A:] is non empty Relation-like set
bool [:(),A:] is non empty set

vSUB Al is non empty functional set

[:(),():] is non empty Relation-like set
bool [:(),():] is non empty set
(@ (xSQ `2)) * S is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
(Al,A,S,(Al,xSQ,A,S)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
VERUM Al is Element of CQC-WFF Al
(Al,xSQ) is Element of CQC-WFF Al

[(VERUM Al),xSQ] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
{(VERUM Al),xSQ} is non empty set
{(VERUM Al)} is non empty trivial 1 -element set
{{(VERUM Al),xSQ},{(VERUM Al)}} is non empty set
Al is non empty Relation-like QC-alphabet
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
A is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
J is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT

dom xSQ is V45() V46() V47() V48() V49() V50() V63() A -element Element of bool NAT
xSQ . J is set
rng xSQ is Element of bool ()
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
A is Element of CQC-Sub-WFF Al
CQC_Sub A is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
(Al,A) is Element of CQC-WFF Al
the_pred_symbol_of (Al,A) is Element of QC-pred_symbols Al
QC-pred_symbols Al is non empty set

QC-variables Al is non empty set

vSUB Al is non empty functional set

(the_pred_symbol_of (Al,A)) ! (CQC_Subst (,(A `2))) is Element of QC-WFF Al
[:(),(QC-WFF Al):] is non empty Relation-like set
bool [:(),(QC-WFF Al):] is non empty set
VERUM Al is Element of CQC-WFF Al

J . A is Element of QC-WFF Al
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
vSUB Al is non empty functional set
A is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
A -ary_QC-pred_symbols Al is non empty Element of bool ()
bool () is non empty set
J is Element of A -ary_QC-pred_symbols Al
xSQ is Element of A -ary_QC-pred_symbols Al

Sub_P (J,S,v) is Sub_atomic Element of QC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set

Sub_P (xSQ,xSQ,S1) is Sub_atomic Element of QC-Sub-WFF Al

z is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
z -ary_QC-pred_symbols Al is non empty Element of bool ()

q is Element of z -ary_QC-pred_symbols Al

Sub_P (q,p,a) is Sub_atomic Element of QC-Sub-WFF Al
J ! S is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set

q ! p is Element of QC-WFF Al

[(J ! S),v] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
{(J ! S),v} is non empty set
{(J ! S)} is non empty trivial 1 -element set
{{(J ! S),v},{(J ! S)}} is non empty set
[(q ! p),a] is V1() Element of [:(QC-WFF Al),(vSUB Al):]
[:(QC-WFF Al),(vSUB Al):] is non empty Relation-like set
{(q ! p),a} is non empty set
{(q ! p)} is non empty trivial 1 -element set
{{(q ! p),a},{(q ! p)}} is non empty set
(<*q*> ^ p) . 1 is set
(<*J*> ^ S) . 1 is set
x is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
x -ary_QC-pred_symbols Al is non empty Element of bool ()

b is Element of x -ary_QC-pred_symbols Al

Sub_P (b,x,e2) is Sub_atomic Element of QC-Sub-WFF Al
xSQ ! xSQ is Element of CQC-WFF Al

b ! x is Element of QC-WFF Al

[(xSQ ! xSQ),S1] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
{(xSQ ! xSQ),S1} is non empty set
{(xSQ ! xSQ)} is non empty trivial 1 -element set
{{(xSQ ! xSQ),S1},{(xSQ ! xSQ)}} is non empty set
[(b ! x),e2] is V1() Element of [:(QC-WFF Al),(vSUB Al):]
{(b ! x),e2} is non empty set
{(b ! x)} is non empty trivial 1 -element set
{{(b ! x),e2},{(b ! x)}} is non empty set
(<*b*> ^ x) . 1 is set
(<*xSQ*> ^ xSQ) . 1 is set
A is non empty Relation-like QC-alphabet
QC-pred_symbols A is non empty set
Al is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
Al -ary_QC-pred_symbols A is non empty Element of bool ()
bool () is non empty set
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
bool () is non empty set
vSUB A is non empty functional set
J is Element of Al -ary_QC-pred_symbols A

Sub_P (J,xSQ,S) is Sub_atomic Element of QC-Sub-WFF A
QC-Sub-WFF A is non empty A -Sub-closed set
CQC-Sub-WFF A is non empty Element of bool ()
bool () is non empty set
QC-WFF A is non empty set
CQC-WFF A is non empty Element of bool ()
bool () is non empty set
{ b1 where b1 is Element of QC-Sub-WFF A : b1 `1 is Element of CQC-WFF A } is set
v is Element of QC-Sub-WFF A
v `1 is Element of QC-WFF A
J ! xSQ is Element of CQC-WFF A
[(J ! xSQ),S] is V1() Element of [:(),(vSUB A):]
[:(),(vSUB A):] is non empty Relation-like set
{(J ! xSQ),S} is non empty set
{(J ! xSQ)} is non empty trivial 1 -element set
{{(J ! xSQ),S},{(J ! xSQ)}} is non empty set
(Sub_P (J,xSQ,S)) `1 is Element of QC-WFF A
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
vSUB Al is non empty functional set
A is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
A -ary_QC-pred_symbols Al is non empty Element of bool ()
bool () is non empty set
J is Element of A -ary_QC-pred_symbols Al

(A,Al,J,xSQ,S) is Sub_atomic Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
CQC_Sub (A,Al,J,xSQ,S) is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set

J ! (CQC_Subst (xSQ,S)) is Element of QC-WFF Al
J ! xSQ is Element of CQC-WFF Al
[(J ! xSQ),S] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
{(J ! xSQ),S} is non empty set
{(J ! xSQ)} is non empty trivial 1 -element set
{{(J ! xSQ),S},{(J ! xSQ)}} is non empty set
(A,Al,J,xSQ,S) `2 is Relation-like Function-like Element of vSUB Al
(Al,(A,Al,J,xSQ,S)) is Element of CQC-WFF Al

the_pred_symbol_of (Al,(A,Al,J,xSQ,S)) is Element of QC-pred_symbols Al
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
vSUB Al is non empty functional set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
A is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
A -ary_QC-pred_symbols Al is non empty Element of bool ()
bool () is non empty set
J is Element of A -ary_QC-pred_symbols Al

J ! (CQC_Subst (xSQ,S)) is Element of QC-WFF Al
(A,Al,J,xSQ,S) is Sub_atomic Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
CQC_Sub (A,Al,J,xSQ,S) is Element of CQC-WFF Al
Al is non empty Relation-like QC-alphabet
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
vSUB Al is non empty functional set
A is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT

len S is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
len (@ S) is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
len xSQ is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
Al is non empty Relation-like QC-alphabet
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
A is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
vSUB Al is non empty functional set

Al is non empty Relation-like QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool ()
bool () is non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
A is Element of bound_QC-variables Al
J is non empty set
Valuations_in (Al,J) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,J

xSQ . A is Element of J
S is Element of CQC-Sub-WFF Al

vSUB Al is non empty functional set
proj1 (S `2) is set
(Al,S,J,xSQ) is Relation-like bound_QC-variables Al -defined J -valued Function-like Element of bool [:(),J:]
[:(),J:] is non empty Relation-like set
bool [:(),J:] is non empty set

[:(),():] is non empty Relation-like set
bool [:(),():] is non empty set
(@ (S `2)) * xSQ is Relation-like bound_QC-variables Al -defined J -valued Function-like Element of bool [:(),J:]
(Al,J,xSQ,(Al,S,J,xSQ)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined J -valued Function-like quasi_total Element of Valuations_in (Al,J)
(Al,J,xSQ,(Al,S,J,xSQ)) . A is Element of J
dom (@ (S `2)) is Element of bool ()
bool () is non empty set
dom ((@ (S `2)) * xSQ) is Element of bool ()
dom (Al,S,J,xSQ) is Element of bool ()
Al is non empty Relation-like QC-alphabet
QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of bool ()
bool () is non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
A is Element of bound_QC-variables Al
J is non empty set
Valuations_in (Al,J) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,J

S is Element of CQC-Sub-WFF Al

vSUB Al is non empty functional set
proj1 (S `2) is set
(Al,S,J,xSQ) is Relation-like bound_QC-variables Al -defined J -valued Function-like Element of bool [:(),J:]
[:(),J:] is non empty Relation-like set
bool [:(),J:] is non empty set

[:(),():] is non empty Relation-like set
bool [:(),():] is non empty set
(@ (S `2)) * xSQ is Relation-like bound_QC-variables Al -defined J -valued Function-like Element of bool [:(),J:]
(Al,J,xSQ,(Al,S,J,xSQ)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined J -valued Function-like quasi_total Element of Valuations_in (Al,J)
(Al,J,xSQ,(Al,S,J,xSQ)) . A is Element of J
(Al,S,J,xSQ) . A is set
dom (@ (S `2)) is Element of bool ()
bool () is non empty set
rng (@ (S `2)) is Element of bool ()
dom xSQ is Element of bool ()
dom (Al,S,J,xSQ) is Element of bool ()
Al is non empty Relation-like QC-alphabet
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
QC-pred_symbols Al is non empty set
vSUB Al is non empty functional set
A is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
A -ary_QC-pred_symbols Al is non empty Element of bool ()
bool () is non empty set
J is non empty set
Valuations_in (Al,J) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,J

S is Element of A -ary_QC-pred_symbols Al

(A,Al,S,xSQ,v) is Sub_atomic Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
(Al,(A,Al,S,xSQ,v),J,xSQ) is Relation-like bound_QC-variables Al -defined J -valued Function-like Element of bool [:(),J:]
[:(),J:] is non empty Relation-like set
bool [:(),J:] is non empty set
(A,Al,S,xSQ,v) `2 is Relation-like Function-like Element of vSUB Al
@ ((A,Al,S,xSQ,v) `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(),():]
[:(),():] is non empty Relation-like set
bool [:(),():] is non empty set
(@ ((A,Al,S,xSQ,v) `2)) * xSQ is Relation-like bound_QC-variables Al -defined J -valued Function-like Element of bool [:(),J:]
(Al,J,xSQ,(Al,(A,Al,S,xSQ,v),J,xSQ)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined J -valued Function-like quasi_total Element of Valuations_in (Al,J)
(Al,J,xSQ,(Al,(A,Al,S,xSQ,v),J,xSQ)) *' xSQ is Relation-like NAT -defined J -valued Function-like FinSequence-like FinSequence of J

len xSQ is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
S ! xSQ is Element of CQC-WFF Al
[(S ! xSQ),v] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
{(S ! xSQ),v} is non empty set
{(S ! xSQ)} is non empty trivial 1 -element set
{{(S ! xSQ),v},{(S ! xSQ)}} is non empty set
len ((Al,J,xSQ,(Al,(A,Al,S,xSQ,v),J,xSQ)) *' xSQ) is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
dom ((Al,J,xSQ,(Al,(A,Al,S,xSQ,v),J,xSQ)) *' xSQ) is V45() V46() V47() V48() V49() V50() V63() Element of bool NAT
Seg A is V45() V46() V47() V48() V49() V50() V63() Element of bool NAT

((Al,J,xSQ,(Al,(A,Al,S,xSQ,v),J,xSQ)) *' xSQ) . q is set
(xSQ *' (CQC_Subst (xSQ,v))) . q is set
p is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
Seg (len xSQ) is V45() V46() V47() V48() V49() V50() V63() Element of bool NAT
dom xSQ is V45() V46() V47() V48() V49() V50() V63() A -element Element of bool NAT
xSQ . p is set
proj1 v is set
(Al,J,xSQ,(Al,(A,Al,S,xSQ,v),J,xSQ)) . (xSQ . p) is set
a is Element of bound_QC-variables Al
(Al,(A,Al,S,xSQ,v),J,xSQ) . a is set
dom (@ ((A,Al,S,xSQ,v) `2)) is Element of bool ()
bool () is non empty set
(@ ((A,Al,S,xSQ,v) `2)) . (xSQ . p) is set
xSQ . ((@ ((A,Al,S,xSQ,v) `2)) . (xSQ . p)) is set
((A,Al,S,xSQ,v) `2) . (xSQ . p) is set
xSQ . (((A,Al,S,xSQ,v) `2) . (xSQ . p)) is set
((Al,J,xSQ,(Al,(A,Al,S,xSQ,v),J,xSQ)) *' xSQ) . p is set
(CQC_Subst (xSQ,v)) . p is set
xSQ . ((CQC_Subst (xSQ,v)) . p) is set
xSQ . (xSQ . p) is set
xSQ . a is Element of J
(xSQ *' (CQC_Subst (xSQ,v))) . p is set
len (xSQ *' (CQC_Subst (xSQ,v))) is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
vSUB Al is non empty functional set
A is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
A -ary_QC-pred_symbols Al is non empty Element of bool ()
bool () is non empty set
J is Element of A -ary_QC-pred_symbols Al

J ! xSQ is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set

(A,Al,J,xSQ,S) is Sub_atomic Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
(Al,(A,Al,J,xSQ,S)) is Element of CQC-WFF Al
[(J ! xSQ),S] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
{(J ! xSQ),S} is non empty set
{(J ! xSQ)} is non empty trivial 1 -element set
{{(J ! xSQ),S},{(J ! xSQ)}} is non empty set
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
vSUB Al is non empty functional set
A is ext-real epsilon-transitive epsilon-connected ordinal natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal Element of NAT
A -ary_QC-pred_symbols Al is non empty Element of bool ()
bool () is non empty set
J is non empty set
K367(J) is set
Valuations_in (Al,J) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,J

S is Element of A -ary_QC-pred_symbols Al

(A,Al,S,xSQ,v) is Sub_atomic Element of CQC-Sub-WFF Al
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
CQC_Sub (A,Al,S,xSQ,v) is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set

S ! (CQC_Subst (xSQ,v)) is Element of CQC-WFF Al

(Al,(A,Al,S,xSQ,v),J,a) is Relation-like bound_QC-variables Al -defined J -valued Function-like Element of bool [:(),J:]
[:(),J:] is non empty Relation-like set
bool [:(),J:] is non empty set
(A,Al,S,xSQ,v) `2 is Relation-like Function-like Element of vSUB Al
@ ((A,Al,S,xSQ,v) `2) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -valued Function-like Element of bool [:(),():]
[:(),():] is non empty Relation-like set
bool [:(),():] is non empty set
(@ ((A,Al,S,xSQ,v) `2)) * a is Relation-like bound_QC-variables Al -defined J -valued Function-like Element of bool [:(),J:]
(Al,J,a,(Al,(A,Al,S,xSQ,v),J,a)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined J -valued Function-like quasi_total Element of Valuations_in (Al,J)
q is Element of CQC-WFF Al
Valid (q,xSQ) is Relation-like Valuations_in (Al,J) -defined K370() -valued Function-like quasi_total Element of Funcs ((Valuations_in (Al,J)),K370())
Funcs ((Valuations_in (Al,J)),K370()) is non empty FUNCTION_DOMAIN of Valuations_in (Al,J),K370()
(Valid (q,xSQ)) . a is Element of K370()

xSQ . S is Element of K367(J)
(Al,J,a,(Al,(A,Al,S,xSQ,v),J,a)) *' xSQ is Relation-like NAT -defined J -valued Function-like FinSequence-like FinSequence of J
S ! xSQ is Element of CQC-WFF Al
Valid ((S ! xSQ),xSQ) is Relation-like Valuations_in (Al,J) -defined K370() -valued Function-like quasi_total Element of Funcs ((Valuations_in (Al,J)),K370())
(Valid ((S ! xSQ),xSQ)) . (Al,J,a,(Al,(A,Al,S,xSQ,v),J,a)) is Element of K370()
(Al,(A,Al,S,xSQ,v)) is Element of CQC-WFF Al
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
A is Element of CQC-Sub-WFF Al

() `1 is Element of QC-WFF Al
QC-WFF Al is non empty set
(Al,A) is Element of CQC-WFF Al
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
'not' (Al,A) is Element of CQC-WFF Al

vSUB Al is non empty functional set

[('not' (Al,A)),(A `2)] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
{('not' (Al,A)),(A `2)} is non empty set
{('not' (Al,A))} is non empty trivial 1 -element set
{{('not' (Al,A)),(A `2)},{('not' (Al,A))}} is non empty set
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
A is Element of CQC-Sub-WFF Al

QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
{ b1 where b1 is Element of QC-Sub-WFF Al : b1 `1 is Element of CQC-WFF Al } is set
xSQ is Element of QC-Sub-WFF Al
xSQ `1 is Element of QC-WFF Al
(Al,A) is Element of CQC-WFF Al
'not' (Al,A) is Element of CQC-WFF Al
() `1 is Element of QC-WFF Al
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
A is non empty set
K367(A) is set
Valuations_in (Al,A) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,A

S is Element of CQC-Sub-WFF Al
(Al,S,A,xSQ) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
[:(),A:] is non empty Relation-like set
bool [:(),A:] is non empty set

vSUB Al is non empty functional set

[:(),():] is non empty Relation-like set
bool [:(),():] is non empty set
(@ (S `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
(Al,A,xSQ,(Al,S,A,xSQ)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
(Al,S) is Sub_negative Element of CQC-Sub-WFF Al
(Al,S) is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
'not' (Al,S) is Element of CQC-WFF Al
(Al,(Al,S)) is Element of CQC-WFF Al
Al is non empty Relation-like QC-alphabet
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
A is non empty set
Valuations_in (Al,A) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,A

xSQ is Element of CQC-Sub-WFF Al
(Al,xSQ,A,J) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
[:(),A:] is non empty Relation-like set
bool [:(),A:] is non empty set

vSUB Al is non empty functional set

[:(),():] is non empty Relation-like set
bool [:(),():] is non empty set
(@ (xSQ `2)) * J is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
(Al,xSQ) is Sub_negative Element of CQC-Sub-WFF Al
(Al,(Al,xSQ),A,J) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
(Al,xSQ) `2 is Relation-like Function-like Element of vSUB Al

(@ ((Al,xSQ) `2)) * J is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
(Al,xSQ) is Element of CQC-WFF Al
'not' (Al,xSQ) is Element of CQC-WFF Al
[('not' (Al,xSQ)),(xSQ `2)] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
{('not' (Al,xSQ)),(xSQ `2)} is non empty set
{('not' (Al,xSQ))} is non empty trivial 1 -element set
{{('not' (Al,xSQ)),(xSQ `2)},{('not' (Al,xSQ))}} is non empty set
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
A is non empty set
K367(A) is set
Valuations_in (Al,A) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,A

xSQ is Element of CQC-Sub-WFF Al
CQC_Sub xSQ is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
(Al,xSQ) is Sub_negative Element of CQC-Sub-WFF Al
CQC_Sub (Al,xSQ) is Element of CQC-WFF Al

(Al,(Al,xSQ),A,S) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
[:(),A:] is non empty Relation-like set
bool [:(),A:] is non empty set
(Al,xSQ) `2 is Relation-like Function-like Element of vSUB Al
vSUB Al is non empty functional set

[:(),():] is non empty Relation-like set
bool [:(),():] is non empty set
(@ ((Al,xSQ) `2)) * S is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
(Al,A,S,(Al,(Al,xSQ),A,S)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
'not' (CQC_Sub xSQ) is Element of CQC-WFF Al
(Al,xSQ,A,S) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]

(@ (xSQ `2)) * S is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
(Al,A,S,(Al,xSQ,A,S)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
A is Element of CQC-Sub-WFF Al

vSUB Al is non empty functional set
J is Element of CQC-Sub-WFF Al

Sub_& (A,J) is Element of QC-Sub-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
{ b1 where b1 is Element of QC-Sub-WFF Al : b1 `1 is Element of CQC-WFF Al } is set
S is Element of QC-Sub-WFF Al
S `1 is Element of QC-WFF Al
(Al,A) is Element of CQC-WFF Al
(Al,J) is Element of CQC-WFF Al
(Al,A) '&' (Al,J) is Element of CQC-WFF Al
[((Al,A) '&' (Al,J)),(A `2)] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
{((Al,A) '&' (Al,J)),(A `2)} is non empty set
{((Al,A) '&' (Al,J))} is non empty trivial 1 -element set
{{((Al,A) '&' (Al,J)),(A `2)},{((Al,A) '&' (Al,J))}} is non empty set
(Sub_& (A,J)) `1 is Element of QC-WFF Al
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
A is Element of CQC-Sub-WFF Al

vSUB Al is non empty functional set
(Al,A) is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
J is Element of CQC-Sub-WFF Al

(Al,A,J) is Element of CQC-Sub-WFF Al
(Al,(Al,A,J)) is Element of CQC-WFF Al
(Al,J) is Element of CQC-WFF Al
(Al,A) '&' (Al,J) is Element of CQC-WFF Al
(Al,A,J) `2 is Relation-like Function-like Element of vSUB Al
Sub_& (A,J) is Element of QC-Sub-WFF Al
[((Al,A) '&' (Al,J)),(A `2)] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
{((Al,A) '&' (Al,J)),(A `2)} is non empty set
{((Al,A) '&' (Al,J))} is non empty trivial 1 -element set
{{((Al,A) '&' (Al,J)),(A `2)},{((Al,A) '&' (Al,J))}} is non empty set
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
A is Element of CQC-Sub-WFF Al

vSUB Al is non empty functional set
J is Element of CQC-Sub-WFF Al

(Al,A,J) is Element of CQC-Sub-WFF Al
(Al,A,J) `2 is Relation-like Function-like Element of vSUB Al
Sub_& (A,J) is Element of QC-Sub-WFF Al
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
(Al,A) is Element of CQC-WFF Al
(Al,J) is Element of CQC-WFF Al
(Al,A) '&' (Al,J) is Element of CQC-WFF Al
[((Al,A) '&' (Al,J)),(A `2)] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
{((Al,A) '&' (Al,J)),(A `2)} is non empty set
{((Al,A) '&' (Al,J))} is non empty trivial 1 -element set
{{((Al,A) '&' (Al,J)),(A `2)},{((Al,A) '&' (Al,J))}} is non empty set
Al is non empty Relation-like QC-alphabet
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
A is non empty set
Valuations_in (Al,A) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
xSQ is Element of CQC-Sub-WFF Al

vSUB Al is non empty functional set
S is Element of CQC-Sub-WFF Al

(Al,xSQ,A,J) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
[:(),A:] is non empty Relation-like set
bool [:(),A:] is non empty set

[:(),():] is non empty Relation-like set
bool [:(),():] is non empty set
(@ (xSQ `2)) * J is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
(Al,xSQ,S) is Element of CQC-Sub-WFF Al
(Al,(Al,xSQ,S),A,J) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
(Al,xSQ,S) `2 is Relation-like Function-like Element of vSUB Al

(@ ((Al,xSQ,S) `2)) * J is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
(Al,S,A,J) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]

Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
A is Element of CQC-Sub-WFF Al

vSUB Al is non empty functional set
CQC_Sub A is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
J is Element of CQC-Sub-WFF Al

(Al,A,J) is Element of CQC-Sub-WFF Al
CQC_Sub (Al,A,J) is Element of CQC-WFF Al
CQC_Sub J is Element of CQC-WFF Al
() '&' () is Element of CQC-WFF Al
Sub_& (A,J) is Element of QC-Sub-WFF Al
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
A is non empty set
K367(A) is set
Valuations_in (Al,A) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,A

S is Element of CQC-Sub-WFF Al

vSUB Al is non empty functional set
(Al,S,A,xSQ) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
[:(),A:] is non empty Relation-like set
bool [:(),A:] is non empty set

[:(),():] is non empty Relation-like set
bool [:(),():] is non empty set
(@ (S `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
(Al,A,xSQ,(Al,S,A,xSQ)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
xSQ is Element of CQC-Sub-WFF Al

(Al,xSQ,A,xSQ) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]

(@ (xSQ `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
(Al,A,xSQ,(Al,xSQ,A,xSQ)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
(Al,S,xSQ) is Element of CQC-Sub-WFF Al
(Al,(Al,S,xSQ),A,xSQ) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
(Al,S,xSQ) `2 is Relation-like Function-like Element of vSUB Al

(@ ((Al,S,xSQ) `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
(Al,A,xSQ,(Al,(Al,S,xSQ),A,xSQ)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
(Al,S) is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
(Al,xSQ) is Element of CQC-WFF Al
(Al,S) '&' (Al,xSQ) is Element of CQC-WFF Al
(Al,(Al,S,xSQ)) is Element of CQC-WFF Al
Al is non empty Relation-like QC-alphabet
QC-pred_symbols Al is non empty set
QC-Sub-WFF Al is non empty Al -Sub-closed set
CQC-Sub-WFF Al is non empty Element of bool ()
bool () is non empty set
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
A is non empty set
K367(A) is set
Valuations_in (Al,A) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,A

xSQ is Element of CQC-Sub-WFF Al

vSUB Al is non empty functional set
CQC_Sub xSQ is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
bool (QC-WFF Al) is non empty set
S is Element of CQC-Sub-WFF Al

CQC_Sub S is Element of CQC-WFF Al
(Al,xSQ,S) is Element of CQC-Sub-WFF Al
CQC_Sub (Al,xSQ,S) is Element of CQC-WFF Al

(Al,(Al,xSQ,S),A,xSQ) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
[:(),A:] is non empty Relation-like set
bool [:(),A:] is non empty set
(Al,xSQ,S) `2 is Relation-like Function-like Element of vSUB Al

[:(),():] is non empty Relation-like set
bool [:(),():] is non empty set
(@ ((Al,xSQ,S) `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
(Al,A,xSQ,(Al,(Al,xSQ,S),A,xSQ)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
(Al,xSQ,A,xSQ) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]

(@ (xSQ `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
(Al,A,xSQ,(Al,xSQ,A,xSQ)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
(Al,S,A,xSQ) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]

(@ (S `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(),A:]
(Al,A,xSQ,(Al,S,A,xSQ)) is Relation-like bound_QC-variables Al -defined bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)
(CQC_Sub xSQ) '&' () is Element of CQC-WFF Al
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
[:(),():] is non empty Relation-like set
A is Element of [:(),():]
A `2 is Element of bound_QC-variables Al
A `1 is Element of QC-Sub-WFF Al
(A `1) `1 is Element of QC-WFF Al
QC-WFF Al is non empty set
All ((A `2),((A `1) `1)) is Element of QC-WFF Al

Sub_All (A,J) is Element of QC-Sub-WFF Al
(Sub_All (A,J)) `1 is Element of QC-WFF Al
(Sub_All (A,J)) `2 is Relation-like Function-like Element of vSUB Al
vSUB Al is non empty functional set
[(All ((A `2),((A `1) `1))),J] is V1() Element of [:(QC-WFF Al),(vSUB Al):]
[:(QC-WFF Al),(vSUB Al):] is non empty Relation-like set
{(All ((A `2),((A `1) `1))),J} is non empty set
{(All ((A `2),((A `1) `1)))} is non empty trivial 1 -element set
{{(All ((A `2),((A `1) `1))),J},{(All ((A `2),((A `1) `1)))}} is non empty set
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
[:(),():] is non empty Relation-like set
Al is non empty Relation-like QC-alphabet
QC-Sub-WFF Al is non empty Al -Sub-closed set
bound_QC-variables Al is non empty Element of bool ()
QC-variables Al is non empty set
bool () is non empty set
[:(),():] is non empty Relation-like set
vSUB Al is non empty functional set

the Element of bound_QC-variables Al is Element of bound_QC-variables Al
CQC-WFF Al is non empty Element of bool (QC-WFF Al)
QC-WFF Al is non empty set
bool (QC-WFF Al) is non empty set
[:(CQC-WFF Al),(vSUB Al):] is non empty Relation-like set
VERUM Al is Element of CQC-WFF Al
[(VERUM Al), the Relation-like Function-like Element of vSUB Al] is V1() Element of [:(CQC-WFF Al),(vSUB Al):]
{(VERUM Al), the Relation-like Function-like Element of vSUB Al} is non empty set
{(VERUM Al)} is non empty trivial 1 -element set
{{(VERUM Al), the Relation-like Function-like Element of vSUB Al},{(VERUM Al)}} is non empty set
[[(VERUM Al), the Relation-like Function-like Element of vSUB Al], the Element of bound_QC-variables Al] is V1() Element of [:[:(CQC-WFF Al),(vSUB Al):],():]
[:[:(CQC-WFF Al),(vSUB Al):],():] is non empty Relation-like set
{[(VERUM Al), the Relation-like Function-like Element of vSUB Al], the Element of bound_QC-variables Al} is non empty set
{[(VERUM Al), the Relation-like Function-like Element of vSUB Al]} is non empty trivial Relation-like Function-like constant 1 -element set
{{[(VERUM Al), the Relation-like Function-like Element of vSUB Al], the Element of bound_QC-variables Al},{[(VERUM Al), the Relation-like Function-like Element of vSUB Al]}} is non empty set
[] is V1() Element of [:,(vSUB Al):]
[:,(vSUB Al):] is non empty Relation-like V52() set
{