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

[:COMPLEX,COMPLEX:] is Relation-like set

bool [:COMPLEX,COMPLEX:] is non empty set

[:COMPLEX,REAL:] is Relation-like set

bool [:COMPLEX,REAL:] is non empty set

K370() is set

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V45() V46() V47() V48() V49() V50() V51() V52() V63() V64() V65() V66() cardinal {} -element Function-yielding V82() set

the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V45() V46() V47() V48() V49() V50() V51() V52() V63() V64() V65() V66() cardinal {} -element Function-yielding V82() set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V45() V46() V47() V48() V49() V50() V51() V52() V63() V64() V65() V66() cardinal {} -element Function-yielding V82() 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 is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() V32() V43() V44() V45() V46() V47() V48() V49() V50() V51() V52() V63() V64() V65() V66() cardinal {} -element Function-yielding V82() Element of NAT

[0,0] is V1() set

{0,0} is non empty functional V45() V46() V47() V48() V49() V50() V61() V63() set

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

{{0,0},{0}} is non empty set

<*[0,0]*> is Relation-like Function-like set

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

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

bool [:NAT,[:NAT,NAT:]:] is non empty V52() set

[0,0] is V1() Element of [:NAT,NAT:]

<*[0,0]*> is Relation-like NAT -defined [:NAT,NAT:] -valued Function-like FinSequence-like FinSequence of [:NAT,NAT:]

[1,0] is V1() Element of [:NAT,NAT:]

{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

<*[1,0]*> is Relation-like NAT -defined [:NAT,NAT:] -valued Function-like FinSequence-like FinSequence of [:NAT,NAT:]

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 [:NAT,NAT:]

{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

<*[2,0]*> is Relation-like NAT -defined [:NAT,NAT:] -valued Function-like FinSequence-like FinSequence of [:NAT,NAT:]

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 [:NAT,NAT:]

{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

<*[3,0]*> is Relation-like NAT -defined [:NAT,NAT:] -valued Function-like FinSequence-like FinSequence of [:NAT,NAT:]

xSQ is Relation-like Function-like set

proj1 xSQ is set

J is Relation-like Function-like set

proj1 J is set

S is Relation-like Function-like set

proj1 S is set

Al is Relation-like Function-like set

A is Relation-like Function-like set

Al +* A is Relation-like Function-like set

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

Al +* xSQ is Relation-like Function-like set

A +* S 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

(proj1 A) \/ (proj1 S) is set

proj1 ((Al +* xSQ) +* (A +* S)) is set

((proj1 Al) \/ (proj1 xSQ)) \/ ((proj1 A) \/ (proj1 S)) is set

proj1 (((Al +* xSQ) +* (A +* S)) +* J) is set

(((proj1 Al) \/ (proj1 xSQ)) \/ ((proj1 A) \/ (proj1 S))) \/ (proj1 J) is set

((proj1 A) \/ (proj1 S)) \/ (proj1 J) is set

((proj1 Al) \/ (proj1 xSQ)) \/ (((proj1 A) \/ (proj1 S)) \/ (proj1 J)) is set

(proj1 S) \/ (proj1 J) is set

(proj1 A) \/ ((proj1 S) \/ (proj1 J)) is set

((proj1 Al) \/ (proj1 xSQ)) \/ ((proj1 A) \/ ((proj1 S) \/ (proj1 J))) is set

(proj1 A) \/ (proj1 J) is set

((proj1 Al) \/ (proj1 xSQ)) \/ ((proj1 A) \/ (proj1 J)) is set

((proj1 Al) \/ (proj1 xSQ)) \/ (proj1 J) is set

(((proj1 Al) \/ (proj1 xSQ)) \/ (proj1 J)) \/ (proj1 A) is set

(proj1 xSQ) \/ (proj1 J) is set

(proj1 Al) \/ ((proj1 xSQ) \/ (proj1 J)) is set

((proj1 Al) \/ ((proj1 xSQ) \/ (proj1 J))) \/ (proj1 A) is set

(proj1 Al) \/ (proj1 J) is set

((proj1 Al) \/ (proj1 J)) \/ (proj1 A) 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) \/ (proj1 A) is set

((proj1 Al) \/ (proj1 A)) \/ (proj1 J) 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 (QC-variables Al)

bool (QC-variables Al) is non empty set

A is Element of bound_QC-variables Al

{A} is non empty trivial 1 -element Element of bool (bound_QC-variables Al)

bool (bound_QC-variables Al) is non empty set

J is Relation-like Function-like set

proj1 J is set

(proj1 J) \ {A} is Element of bool (proj1 J)

bool (proj1 J) is non empty set

J | ((proj1 J) \ {A}) is Relation-like Function-like set

J . A is set

A .--> (J . A) is trivial Relation-like bound_QC-variables Al -defined {A} -defined Function-like one-to-one constant 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 | ((proj1 J) \ {A})) +* (A .--> (J . A)) is Relation-like Function-like set

((proj1 J) \ {A}) \/ {A} is non empty set

(proj1 J) \/ {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)

QC-variables Al is non empty set

bool (QC-variables Al) is non empty set

A is non empty set

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

[:(bound_QC-variables Al),A:] is non empty Relation-like set

bool [:(bound_QC-variables Al),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)

QC-variables Al is non empty set

bool (QC-variables Al) is non empty set

A is non empty set

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

[:(bound_QC-variables Al),A:] is non empty Relation-like set

bool [:(bound_QC-variables Al),A:] is non empty set

J is Relation-like bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)

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

J +* xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like set

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

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

dom (J +* xSQ) is Element of bool (bound_QC-variables Al)

bool (bound_QC-variables Al) is non empty set

dom xSQ is Element of bool (bound_QC-variables Al)

(bound_QC-variables Al) \/ (dom xSQ) is non empty set

S is Relation-like Function-like 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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) 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

{ b

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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) is non empty set

bound_QC-variables Al is non empty Element of bool (QC-variables Al)

QC-variables Al is non empty set

bool (QC-variables Al) 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

A `2 is Relation-like Function-like Element of vSUB Al

vSUB Al is non empty functional set

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

[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set

bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set

xSQ is Relation-like bound_QC-variables Al -defined J -valued Function-like quasi_total Element of Valuations_in (Al,J)

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

[:(bound_QC-variables Al),J:] is non empty Relation-like set

bool [:(bound_QC-variables 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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) 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-Sub-WFF Al),(QC-WFF Al):] is non empty Relation-like set

bool [:(QC-Sub-WFF Al),(QC-WFF Al):] is non empty set

J is Relation-like QC-Sub-WFF Al -defined QC-WFF Al -valued Function-like quasi_total Element of bool [:(QC-Sub-WFF Al),(QC-WFF Al):]

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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) is non empty set

bound_QC-variables Al is non empty Element of bool (QC-variables Al)

QC-variables Al is non empty set

bool (QC-variables Al) 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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) is non empty set

bound_QC-variables Al is non empty Element of bool (QC-variables Al)

QC-variables Al is non empty set

bool (QC-variables Al) 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

J is Relation-like QC-pred_symbols Al -defined K367(A) -valued Function-like quasi_total interpretation of 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

S is Relation-like bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)

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

[:(bound_QC-variables Al),A:] is non empty Relation-like set

bool [:(bound_QC-variables Al),A:] is non empty set

xSQ `2 is Relation-like Function-like Element of vSUB Al

vSUB Al is non empty functional set

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

[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set

bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set

(@ (xSQ `2)) * S is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),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

xSQ is Relation-like Function-like Element of vSUB 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)

QC-variables Al is non empty set

bool (QC-variables 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

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

xSQ is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al

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 (QC-variables 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 (QC-Sub-WFF Al)

bool (QC-Sub-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 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

Sub_the_arguments_of A is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al

QC-variables Al is non empty set

A `2 is Relation-like Function-like Element of vSUB Al

vSUB Al is non empty functional set

CQC_Subst ((Sub_the_arguments_of A),(A `2)) is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al

(the_pred_symbol_of (Al,A)) ! (CQC_Subst ((Sub_the_arguments_of A),(A `2))) is Element of QC-WFF Al

[:(QC-Sub-WFF Al),(QC-WFF Al):] is non empty Relation-like set

bool [:(QC-Sub-WFF Al),(QC-WFF Al):] is non empty set

VERUM Al is Element of CQC-WFF Al

J is Relation-like QC-Sub-WFF Al -defined QC-WFF Al -valued Function-like quasi_total Element of bool [:(QC-Sub-WFF Al),(QC-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)

QC-variables Al is non empty set

bool (QC-variables 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 (QC-pred_symbols Al)

bool (QC-pred_symbols Al) is non empty set

J is Element of A -ary_QC-pred_symbols Al

xSQ is Element of A -ary_QC-pred_symbols Al

S is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al

xSQ is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al

v is Relation-like Function-like Element of vSUB 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_the_arguments_of (Sub_P (J,S,v)) is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al

S1 is Relation-like Function-like Element of vSUB Al

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

Sub_the_arguments_of (Sub_P (xSQ,xSQ,S1)) is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables 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 (QC-pred_symbols Al)

p is Relation-like NAT -defined QC-variables Al -valued Function-like z -element FinSequence-like FinSequence of QC-variables Al

q is Element of z -ary_QC-pred_symbols Al

a is Relation-like Function-like Element of vSUB 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

<*J*> is Relation-like NAT -defined A -ary_QC-pred_symbols Al -valued Function-like FinSequence-like FinSequence of A -ary_QC-pred_symbols Al

<*J*> ^ S is Relation-like Function-like FinSequence-like set

q ! p is Element of QC-WFF Al

<*q*> is Relation-like NAT -defined z -ary_QC-pred_symbols Al -valued Function-like FinSequence-like FinSequence of z -ary_QC-pred_symbols Al

<*q*> ^ p is Relation-like Function-like FinSequence-like set

[(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 (QC-pred_symbols Al)

x is Relation-like NAT -defined QC-variables Al -valued Function-like x -element FinSequence-like FinSequence of QC-variables Al

b is Element of x -ary_QC-pred_symbols Al

e2 is Relation-like Function-like Element of vSUB Al

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

xSQ ! xSQ is Element of CQC-WFF Al

<*xSQ*> is Relation-like NAT -defined A -ary_QC-pred_symbols Al -valued Function-like FinSequence-like FinSequence of A -ary_QC-pred_symbols Al

<*xSQ*> ^ xSQ is Relation-like Function-like FinSequence-like set

b ! x is Element of QC-WFF Al

<*b*> is Relation-like NAT -defined x -ary_QC-pred_symbols Al -valued Function-like FinSequence-like FinSequence of x -ary_QC-pred_symbols Al

<*b*> ^ x is Relation-like Function-like FinSequence-like set

[(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 (QC-pred_symbols A)

bool (QC-pred_symbols A) is non empty set

bound_QC-variables A is non empty Element of bool (QC-variables A)

QC-variables A is non empty set

bool (QC-variables A) is non empty set

vSUB A is non empty functional set

J is Element of Al -ary_QC-pred_symbols A

xSQ is Relation-like NAT -defined bound_QC-variables A -valued QC-variables A -valued Function-like Al -element FinSequence-like FinSequence of QC-variables A

S is Relation-like Function-like Element of vSUB 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 (QC-Sub-WFF A)

bool (QC-Sub-WFF A) is non empty set

QC-WFF A is non empty set

CQC-WFF A is non empty Element of bool (QC-WFF A)

bool (QC-WFF A) is non empty set

{ b

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 [:(CQC-WFF A),(vSUB A):]

[:(CQC-WFF 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)

QC-variables Al is non empty set

bool (QC-variables 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 (QC-pred_symbols Al)

bool (QC-pred_symbols Al) is non empty set

J is Element of A -ary_QC-pred_symbols Al

xSQ is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al

S is Relation-like Function-like Element of vSUB 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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) 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

CQC_Subst (xSQ,S) is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al

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

Sub_the_arguments_of (A,Al,J,xSQ,S) is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables 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)

QC-variables Al is non empty set

bool (QC-variables Al) 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 (QC-pred_symbols Al)

bool (QC-pred_symbols Al) is non empty set

J is Element of A -ary_QC-pred_symbols Al

xSQ is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al

S is Relation-like Function-like Element of vSUB Al

CQC_Subst (xSQ,S) is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables 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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) 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)

QC-variables Al is non empty set

bool (QC-variables 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

J is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al

xSQ is Relation-like Function-like Element of vSUB Al

CQC_Subst (J,xSQ) is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al

S is Relation-like NAT -defined bound_QC-variables Al -valued Function-like FinSequence-like FinSequence of bound_QC-variables Al

CQC_Subst (S,xSQ) is Relation-like NAT -defined bound_QC-variables Al -valued Function-like FinSequence-like FinSequence of bound_QC-variables Al

xSQ is Relation-like NAT -defined bound_QC-variables Al -valued Function-like FinSequence-like FinSequence of bound_QC-variables Al

@ S is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al

CQC_Subst ((@ S),xSQ) is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al

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)

QC-variables Al is non empty set

bool (QC-variables 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

vSUB Al is non empty functional set

J is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al

xSQ is Relation-like Function-like Element of vSUB Al

CQC_Subst (J,xSQ) is Relation-like NAT -defined QC-variables Al -valued Function-like FinSequence-like FinSequence of QC-variables Al

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 (QC-variables Al)

bool (QC-variables 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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) 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 is Relation-like bound_QC-variables Al -defined J -valued Function-like quasi_total Element of Valuations_in (Al,J)

xSQ . A is Element of J

S is Element of CQC-Sub-WFF Al

S `2 is Relation-like Function-like Element of vSUB 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 [:(bound_QC-variables Al),J:]

[:(bound_QC-variables Al),J:] is non empty Relation-like set

bool [:(bound_QC-variables Al),J:] is non empty set

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

[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set

bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set

(@ (S `2)) * xSQ is Relation-like bound_QC-variables Al -defined J -valued Function-like Element of bool [:(bound_QC-variables Al),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 (bound_QC-variables Al)

bool (bound_QC-variables Al) is non empty set

dom ((@ (S `2)) * xSQ) is Element of bool (bound_QC-variables Al)

dom (Al,S,J,xSQ) is Element of bool (bound_QC-variables Al)

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 (QC-variables Al)

bool (QC-variables 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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) 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 is Relation-like bound_QC-variables Al -defined J -valued Function-like quasi_total Element of Valuations_in (Al,J)

S is Element of CQC-Sub-WFF Al

S `2 is Relation-like Function-like Element of vSUB 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 [:(bound_QC-variables Al),J:]

[:(bound_QC-variables Al),J:] is non empty Relation-like set

bool [:(bound_QC-variables Al),J:] is non empty set

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

[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set

bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set

(@ (S `2)) * xSQ is Relation-like bound_QC-variables Al -defined J -valued Function-like Element of bool [:(bound_QC-variables Al),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 (bound_QC-variables Al)

bool (bound_QC-variables Al) is non empty set

rng (@ (S `2)) is Element of bool (bound_QC-variables Al)

dom xSQ is Element of bool (bound_QC-variables Al)

dom (Al,S,J,xSQ) is Element of bool (bound_QC-variables Al)

Al is non empty Relation-like QC-alphabet

bound_QC-variables Al is non empty Element of bool (QC-variables Al)

QC-variables Al is non empty set

bool (QC-variables Al) 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 (QC-pred_symbols Al)

bool (QC-pred_symbols Al) is non empty set

J is non empty set

Valuations_in (Al,J) is non empty FUNCTION_DOMAIN of bound_QC-variables Al,J

xSQ is Relation-like bound_QC-variables Al -defined J -valued Function-like quasi_total Element of Valuations_in (Al,J)

S is Element of A -ary_QC-pred_symbols Al

xSQ is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al

v is Relation-like Function-like Element of vSUB 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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) 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 [:(bound_QC-variables Al),J:]

[:(bound_QC-variables Al),J:] is non empty Relation-like set

bool [:(bound_QC-variables Al),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 [:(bound_QC-variables Al),(bound_QC-variables Al):]

[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set

bool [:(bound_QC-variables Al),(bound_QC-variables Al):] 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 [:(bound_QC-variables Al),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

CQC_Subst (xSQ,v) is Relation-like NAT -defined QC-variables Al -valued bound_QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al

xSQ *' (CQC_Subst (xSQ,v)) 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

q is ext-real epsilon-transitive epsilon-connected ordinal natural V52() cardinal set

((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 (bound_QC-variables Al)

bool (bound_QC-variables Al) 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)

QC-variables Al is non empty set

bool (QC-variables 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 (QC-pred_symbols Al)

bool (QC-pred_symbols Al) is non empty set

J is Element of A -ary_QC-pred_symbols Al

xSQ is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables 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

S is Relation-like Function-like Element of vSUB 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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) 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)

QC-variables Al is non empty set

bool (QC-variables 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 (QC-pred_symbols Al)

bool (QC-pred_symbols Al) 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

xSQ is Relation-like QC-pred_symbols Al -defined K367(J) -valued Function-like quasi_total interpretation of Al,J

S is Element of A -ary_QC-pred_symbols Al

xSQ is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al

v is Relation-like Function-like Element of vSUB 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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) 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

CQC_Subst (xSQ,v) is Relation-like NAT -defined QC-variables Al -valued bound_QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al

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

a is Relation-like bound_QC-variables Al -defined J -valued Function-like quasi_total Element of Valuations_in (Al,J)

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

[:(bound_QC-variables Al),J:] is non empty Relation-like set

bool [:(bound_QC-variables Al),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 [:(bound_QC-variables Al),(bound_QC-variables Al):]

[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set

bool [:(bound_QC-variables Al),(bound_QC-variables Al):] 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 [:(bound_QC-variables Al),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()

p is Relation-like NAT -defined bound_QC-variables Al -valued QC-variables Al -valued Function-like A -element FinSequence-like FinSequence of QC-variables Al

a *' p is Relation-like NAT -defined J -valued Function-like FinSequence-like FinSequence of J

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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) is non empty set

A is Element of CQC-Sub-WFF Al

Sub_not A is Sub_negative Element of QC-Sub-WFF Al

(Sub_not A) `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

(Sub_not A) `2 is Relation-like Function-like Element of vSUB Al

vSUB Al is non empty functional set

A `2 is Relation-like Function-like Element of vSUB Al

[('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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) is non empty set

A is Element of CQC-Sub-WFF Al

Sub_not A is Sub_negative 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

{ b

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

(Sub_not A) `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)

QC-variables Al is non empty set

bool (QC-variables 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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) 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

J is Relation-like QC-pred_symbols Al -defined K367(A) -valued Function-like quasi_total interpretation of Al,A

xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (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 [:(bound_QC-variables Al),A:]

[:(bound_QC-variables Al),A:] is non empty Relation-like set

bool [:(bound_QC-variables Al),A:] is non empty set

S `2 is Relation-like Function-like Element of vSUB Al

vSUB Al is non empty functional set

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

[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set

bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set

(@ (S `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),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)

QC-variables Al is non empty set

bool (QC-variables 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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) is non empty set

A is non empty set

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

J is Relation-like 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,J) is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),A:]

[:(bound_QC-variables Al),A:] is non empty Relation-like set

bool [:(bound_QC-variables Al),A:] is non empty set

xSQ `2 is Relation-like Function-like Element of vSUB Al

vSUB Al is non empty functional set

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

[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set

bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set

(@ (xSQ `2)) * J is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),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 [:(bound_QC-variables Al),A:]

(Al,xSQ) `2 is Relation-like Function-like Element of vSUB Al

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

(@ ((Al,xSQ) `2)) * J is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) is non empty set

bound_QC-variables Al is non empty Element of bool (QC-variables Al)

QC-variables Al is non empty set

bool (QC-variables Al) 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

J is Relation-like QC-pred_symbols Al -defined K367(A) -valued Function-like quasi_total interpretation of 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

S is Relation-like bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)

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

[:(bound_QC-variables Al),A:] is non empty Relation-like set

bool [:(bound_QC-variables Al),A:] is non empty set

(Al,xSQ) `2 is Relation-like Function-like Element of vSUB Al

vSUB Al is non empty functional set

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

[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set

bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set

(@ ((Al,xSQ) `2)) * S is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),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 [:(bound_QC-variables Al),A:]

xSQ `2 is Relation-like Function-like Element of vSUB Al

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

(@ (xSQ `2)) * S is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) is non empty set

A is Element of CQC-Sub-WFF Al

A `2 is Relation-like Function-like Element of vSUB Al

vSUB Al is non empty functional set

J is Element of CQC-Sub-WFF Al

J `2 is Relation-like Function-like Element of vSUB 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

{ b

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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) is non empty set

A is Element of CQC-Sub-WFF Al

A `2 is Relation-like Function-like Element of vSUB 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

J `2 is Relation-like Function-like Element of vSUB 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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) is non empty set

A is Element of CQC-Sub-WFF Al

A `2 is Relation-like Function-like Element of vSUB Al

vSUB Al is non empty functional set

J is Element of CQC-Sub-WFF Al

J `2 is Relation-like Function-like Element of vSUB 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)

QC-variables Al is non empty set

bool (QC-variables Al) 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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) is non empty set

xSQ is Element of CQC-Sub-WFF Al

xSQ `2 is Relation-like Function-like Element of vSUB Al

vSUB Al is non empty functional set

S is Element of CQC-Sub-WFF Al

S `2 is Relation-like Function-like Element of vSUB Al

J is Relation-like bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)

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

[:(bound_QC-variables Al),A:] is non empty Relation-like set

bool [:(bound_QC-variables Al),A:] is non empty set

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

[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set

bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set

(@ (xSQ `2)) * J is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),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 [:(bound_QC-variables Al),A:]

(Al,xSQ,S) `2 is Relation-like Function-like Element of vSUB Al

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

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

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

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

(@ (S `2)) * J is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables 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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) is non empty set

A is Element of CQC-Sub-WFF Al

A `2 is Relation-like Function-like Element of vSUB 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

J `2 is Relation-like Function-like Element of vSUB 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

(CQC_Sub A) '&' (CQC_Sub J) 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)

QC-variables Al is non empty set

bool (QC-variables 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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) 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

J is Relation-like QC-pred_symbols Al -defined K367(A) -valued Function-like quasi_total interpretation of Al,A

xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)

S is Element of CQC-Sub-WFF Al

S `2 is Relation-like Function-like Element of vSUB 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 [:(bound_QC-variables Al),A:]

[:(bound_QC-variables Al),A:] is non empty Relation-like set

bool [:(bound_QC-variables Al),A:] is non empty set

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

[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set

bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set

(@ (S `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),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

xSQ `2 is Relation-like Function-like Element of vSUB Al

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

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

(@ (xSQ `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),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 [:(bound_QC-variables Al),A:]

(Al,S,xSQ) `2 is Relation-like Function-like Element of vSUB Al

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

(@ ((Al,S,xSQ) `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),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 (QC-Sub-WFF Al)

bool (QC-Sub-WFF Al) is non empty set

bound_QC-variables Al is non empty Element of bool (QC-variables Al)

QC-variables Al is non empty set

bool (QC-variables Al) 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

J is Relation-like QC-pred_symbols Al -defined K367(A) -valued Function-like quasi_total interpretation of Al,A

xSQ is Element of CQC-Sub-WFF Al

xSQ `2 is Relation-like Function-like Element of vSUB 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

S `2 is Relation-like Function-like Element of vSUB 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

xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like quasi_total Element of Valuations_in (Al,A)

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

[:(bound_QC-variables Al),A:] is non empty Relation-like set

bool [:(bound_QC-variables Al),A:] is non empty set

(Al,xSQ,S) `2 is Relation-like Function-like Element of vSUB Al

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

[:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty Relation-like set

bool [:(bound_QC-variables Al),(bound_QC-variables Al):] is non empty set

(@ ((Al,xSQ,S) `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),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 [:(bound_QC-variables Al),A:]

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

(@ (xSQ `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),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 [:(bound_QC-variables Al),A:]

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

(@ (S `2)) * xSQ is Relation-like bound_QC-variables Al -defined A -valued Function-like Element of bool [:(bound_QC-variables Al),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) '&' (CQC_Sub S) 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)

QC-variables Al is non empty set

bool (QC-variables Al) is non empty set

[:(QC-Sub-WFF Al),(bound_QC-variables Al):] is non empty Relation-like set

A is Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]

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

J is Relation-like Function-like second_Q_comp of A

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)

QC-variables Al is non empty set

bool (QC-variables Al) is non empty set

[:(QC-Sub-WFF Al),(bound_QC-variables Al):] 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)

QC-variables Al is non empty set

bool (QC-variables Al) is non empty set

[:(QC-Sub-WFF Al),(bound_QC-variables Al):] is non empty Relation-like set

vSUB Al is non empty functional set

the Relation-like Function-like Element of vSUB Al is Relation-like Function-like Element of vSUB Al

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):],(bound_QC-variables Al):]

[:[:(CQC-WFF Al),(vSUB Al):],(bound_QC-variables 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

[<*[0,0]*>, the Relation-like Function-like Element of vSUB Al] is V1() Element of [:(bool [:NAT,[:NAT,NAT:]:]),(vSUB Al):]

[:(bool [:NAT,[:NAT,NAT:]:]),(vSUB Al):] is non empty Relation-like V52() set

{<*[0,0]*>, the Relation-like Function-like