:: VALUAT_1 semantic presentation

REAL is V4() V5() V6() V10() set
NAT is V4() V5() V6() V7() V8() V9() V10() ordinal V40() V45() V46() Element of K24(REAL)
K24(REAL) is set
NAT is V4() V5() V6() V7() V8() V9() V10() ordinal V40() V45() V46() set
K24(NAT) is V40() set
K24(NAT) is V40() set
BOOLEAN is non empty set
{} is V4() V5() V6() V7() V8() V9() V10() Function-like functional empty ordinal V45() V47( {} ) V53() set
1 is ext-real V4() V5() V6() V7() V8() V9() non empty ordinal natural V40() V45() Element of NAT
0 is ext-real non positive non negative V4() V5() V6() V7() V8() V9() V10() Function-like functional empty ordinal natural V40() V45() V47( {} ) V53() Element of NAT

K143() is set
K144() is set

bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
A is set
Funcs ((),A) is functional set

A is non empty set
(Al,A) is set
bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
Funcs ((),A) is functional non empty set

bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
A is non empty set
(Al,A) is functional non empty set
Funcs ((),A) is functional non empty set
K25((),A) is set
K24(K25((),A)) is set
x is set

dom y is set
rng y is set

A is non empty set
(Al,A) is functional non empty set
bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
Funcs ((),A) is functional non empty set
K25((),A) is set
K24(K25((),A)) is set
x is Relation-like Function-like Element of (Al,A)

QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24(())
K24(()) is set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
y is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
x is Element of bound_QC-variables Al
{ (y . b1) where b1 is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A) : for b2 being Element of bound_QC-variables Al holds
( x = b2 or b1 . b2 = a1 . b2 )
}
is set

ALL { (y . b1) where b1 is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A) : for b2 being Element of bound_QC-variables Al holds
( x = b2 or b1 . b2 = a1 . b2 )
}
is boolean Element of BOOLEAN

K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set
p is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
dom p is set
rng p is set
q is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)

q . J is boolean Element of BOOLEAN
{ (y . b1) where b1 is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A) : for b2 being Element of bound_QC-variables Al holds
( x = b2 or b1 . b2 = J . b2 )
}
is set

ALL { (y . b1) where b1 is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A) : for b2 being Element of bound_QC-variables Al holds
( x = b2 or b1 . b2 = J . b2 )
}
is boolean Element of BOOLEAN

p is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
q is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)

p . J is boolean Element of BOOLEAN
q . J is boolean Element of BOOLEAN
{ (y . b1) where b1 is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A) : for b2 being Element of bound_QC-variables Al holds
( x = b2 or b1 . b2 = J . b2 )
}
is set

ALL { (y . b1) where b1 is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A) : for b2 being Element of bound_QC-variables Al holds
( x = b2 or b1 . b2 = J . b2 )
}
is boolean Element of BOOLEAN

QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24(())
K24(()) is set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
x is Element of bound_QC-variables Al

p is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,p) . y is boolean Element of BOOLEAN
{ (p . b1) where b1 is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A) : for b2 being Element of bound_QC-variables Al holds
( x = b2 or b1 . b2 = y . b2 )
}
is set

p . q is boolean Element of BOOLEAN
ALL { (p . b1) where b1 is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A) : for b2 being Element of bound_QC-variables Al holds
( x = b2 or b1 . b2 = y . b2 )
}
is boolean Element of BOOLEAN

p . q is boolean Element of BOOLEAN

p . J is boolean Element of BOOLEAN

QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24(())
K24(()) is set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
x is Element of bound_QC-variables Al

p is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,p) . y is boolean Element of BOOLEAN
{ (p . b1) where b1 is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A) : for b2 being Element of bound_QC-variables Al holds
( x = b2 or b1 . b2 = y . b2 )
}
is set

ALL { (p . b1) where b1 is Relation-like bound_QC-variables Al -defined A -valued Function-like V24( bound_QC-variables Al) quasi_total Element of (Al,A) : for b2 being Element of bound_QC-variables Al holds
( x = b2 or b1 . b2 = y . b2 )
}
is boolean Element of BOOLEAN

p . q is boolean Element of BOOLEAN

p . q is boolean Element of BOOLEAN

p . q is boolean Element of BOOLEAN

p . J is boolean Element of BOOLEAN

bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
x is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set

bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
x is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set

rng p is set
rng (y * p) is set
len y is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
dom p is set
rng y is set
dom (y * p) is set
dom y is V4() V5() V6() V7() V8() V9() V47(x) Element of K24(NAT)
Seg x is V4() V5() V6() V7() V8() V9() Element of K24(NAT)

len q is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
len y is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
dom p is set
rng y is set
dom y is V4() V5() V6() V7() V8() V9() V47(x) Element of K24(NAT)
dom q is V4() V5() V6() V7() V8() V9() Element of K24(NAT)

q . J is set
y . J is set
p . (y . J) is set
dom q is V4() V5() V6() V7() V8() V9() Element of K24(NAT)
dom y is V4() V5() V6() V7() V8() V9() V47(x) Element of K24(NAT)
J is set
y . J is set
J is set
q . J is set
y . J is set
p . (y . J) is set
s is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT

bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
x is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
A is non empty set
relations_on A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN

p is Element of relations_on A
q is set

(Al,A,x,y,J) is Relation-like NAT -defined A -valued Function-like FinSequence-like FinSequence of A
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set
q is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
dom q is set
rng q is set
J is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)

(Al,A,x,y,s) is Relation-like NAT -defined A -valued Function-like FinSequence-like FinSequence of A
J . s is boolean Element of BOOLEAN

(Al,A,x,y,v) is Relation-like NAT -defined A -valued Function-like FinSequence-like FinSequence of A
q is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
J is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)

q . s is boolean Element of BOOLEAN
J . s is boolean Element of BOOLEAN
(Al,A,x,y,s) is Relation-like NAT -defined A -valued Function-like FinSequence-like FinSequence of A
(Al,A,x,y,s) is Relation-like NAT -defined A -valued Function-like FinSequence-like FinSequence of A
(Al,A,x,y,s) is Relation-like NAT -defined A -valued Function-like FinSequence-like FinSequence of A

CQC-WFF Al is non empty Element of K24((QC-WFF Al))
QC-WFF Al is non empty set
K24((QC-WFF Al)) is set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
Funcs ((),A) is functional non empty set
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
K25((CQC-WFF Al),(Funcs ((Al,A),BOOLEAN))) is set
K24(K25((CQC-WFF Al),(Funcs ((Al,A),BOOLEAN)))) is set
x is Relation-like CQC-WFF Al -defined Funcs ((Al,A),BOOLEAN) -valued Function-like non empty V24( CQC-WFF Al) quasi_total Element of K24(K25((CQC-WFF Al),(Funcs ((Al,A),BOOLEAN))))
y is Element of CQC-WFF Al

x . y is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)

QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
K25((),()) is set
K24(K25((),())) is set

y is Element of QC-pred_symbols Al
x . y is Element of relations_on A
the_arity_of y is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
p is Element of relations_on A
the_arity_of p is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT

QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
x is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
x -ary_QC-pred_symbols Al is non empty Element of K24(())
K24(()) is set

p is Element of x -ary_QC-pred_symbols Al
y . p is set

QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
Funcs ((),A) is functional non empty set
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
K25((CQC-WFF Al),(Funcs ((Al,A),BOOLEAN))) is set
K24(K25((CQC-WFF Al),(Funcs ((Al,A),BOOLEAN)))) is set
y is Element of CQC-WFF Al
VERUM Al is Element of CQC-WFF Al
(Al,A) --> TRUE is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set

In (((Al,A) --> TRUE),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
J is Relation-like CQC-WFF Al -defined Funcs ((Al,A),BOOLEAN) -valued Function-like non empty V24( CQC-WFF Al) quasi_total Element of K24(K25((CQC-WFF Al),(Funcs ((Al,A),BOOLEAN))))
(Al,A,J,(VERUM Al)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
s is Element of CQC-WFF Al
'not' s is Element of CQC-WFF Al
(Al,A,J,()) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,s) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
'not' (Al,A,J,s) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
v is Element of CQC-WFF Al
s '&' v is Element of CQC-WFF Al
(Al,A,J,(s '&' v)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,v) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,J,s) '&' (Al,A,J,v) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
w is Element of bound_QC-variables Al
All (w,s) is Element of CQC-WFF Al
(Al,A,J,(All (w,s))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,w,(Al,A,J,s)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
l3 is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
l3 -ary_QC-pred_symbols Al is non empty Element of K24(())
K24(()) is set

y is Element of l3 -ary_QC-pred_symbols Al
y ! x is Element of CQC-WFF Al
(Al,A,J,(y ! x)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,l3,x,y) is Element of relations_on A
(Al,A,l3,x,(Al,A,l3,x,y)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
In (('not' (Al,A,J,s)),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
In (((Al,A,J,s) '&' (Al,A,J,v)),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
In ((Al,A,w,(Al,A,J,s)),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
In (((Al,A) --> TRUE),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
J is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
s is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
v is Relation-like CQC-WFF Al -defined Funcs ((Al,A),BOOLEAN) -valued Function-like non empty V24( CQC-WFF Al) quasi_total Element of K24(K25((CQC-WFF Al),(Funcs ((Al,A),BOOLEAN))))
(Al,A,v,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,v,(VERUM Al)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
y is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
y -ary_QC-pred_symbols Al is non empty Element of K24(())
K24(()) is set
q is Element of y -ary_QC-pred_symbols Al

q ! p is Element of CQC-WFF Al
(Al,A,v,(q ! p)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,y,x,q) is Element of relations_on A
(Al,A,y,p,(Al,A,y,x,q)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
w is Element of CQC-WFF Al
(Al,A,v,w) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
'not' (Al,A,v,w) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
'not' w is Element of CQC-WFF Al
(Al,A,v,()) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
In (('not' (Al,A,v,w)),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
l3 is Element of CQC-WFF Al
(Al,A,v,l3) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,v,w) '&' (Al,A,v,l3) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
w '&' l3 is Element of CQC-WFF Al
(Al,A,v,(w '&' l3)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
In (((Al,A,v,w) '&' (Al,A,v,l3)),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
x is Element of bound_QC-variables Al
All (x,w) is Element of CQC-WFF Al
(Al,A,v,(All (x,w))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,(Al,A,v,w)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
In ((Al,A,x,(Al,A,v,w)),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
w is Relation-like CQC-WFF Al -defined Funcs ((Al,A),BOOLEAN) -valued Function-like non empty V24( CQC-WFF Al) quasi_total Element of K24(K25((CQC-WFF Al),(Funcs ((Al,A),BOOLEAN))))
(Al,A,w,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,w,(VERUM Al)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
p is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
p -ary_QC-pred_symbols Al is non empty Element of K24(())
v is Element of p -ary_QC-pred_symbols Al

v ! q is Element of CQC-WFF Al
(Al,A,w,(v ! q)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,x,v) is Element of relations_on A
(Al,A,p,q,(Al,A,p,x,v)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
l3 is Element of CQC-WFF Al
(Al,A,w,l3) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
'not' (Al,A,w,l3) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
'not' l3 is Element of CQC-WFF Al
(Al,A,w,('not' l3)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
In (('not' (Al,A,w,l3)),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
x is Element of CQC-WFF Al
(Al,A,w,x) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,w,l3) '&' (Al,A,w,x) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
l3 '&' x is Element of CQC-WFF Al
(Al,A,w,(l3 '&' x)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
In (((Al,A,w,l3) '&' (Al,A,w,x)),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)
y is Element of bound_QC-variables Al
All (y,l3) is Element of CQC-WFF Al
(Al,A,w,(All (y,l3))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,y,(Al,A,w,l3)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
In ((Al,A,y,(Al,A,w,l3)),(Funcs ((Al,A),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,A),BOOLEAN)

QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
VERUM Al is Element of CQC-WFF Al
bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
A is Element of CQC-WFF Al
x is non empty set
relations_on x is non empty set
(Al,x) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,x
Funcs ((),x) is functional non empty set
(Al,x) --> TRUE is Relation-like (Al,x) -defined BOOLEAN -valued Function-like non empty V24((Al,x)) quasi_total boolean-valued Element of K24(K25((Al,x),BOOLEAN))
K25((Al,x),BOOLEAN) is set
K24(K25((Al,x),BOOLEAN)) is set

(Al,x,y,(VERUM Al)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
Funcs ((Al,x),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,x), BOOLEAN
(Al,x,y,A) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
In (((Al,x) --> TRUE),(Funcs ((Al,x),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,x),BOOLEAN)
K25((CQC-WFF Al),(Funcs ((Al,x),BOOLEAN))) is set
K24(K25((CQC-WFF Al),(Funcs ((Al,x),BOOLEAN)))) is set
J is Element of CQC-WFF Al
(Al,x,y,J) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
s is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
v is Relation-like CQC-WFF Al -defined Funcs ((Al,x),BOOLEAN) -valued Function-like non empty V24( CQC-WFF Al) quasi_total Element of K24(K25((CQC-WFF Al),(Funcs ((Al,x),BOOLEAN))))
(Al,x,v,J) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,v,(VERUM Al)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
w is Element of CQC-WFF Al
'not' w is Element of CQC-WFF Al
(Al,x,v,()) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,v,w) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
'not' (Al,x,v,w) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like non empty V24((Al,x)) quasi_total boolean-valued Element of K24(K25((Al,x),BOOLEAN))
In (('not' (Al,x,v,w)),(Funcs ((Al,x),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,x),BOOLEAN)
l3 is Element of CQC-WFF Al
w '&' l3 is Element of CQC-WFF Al
(Al,x,v,(w '&' l3)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,v,l3) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,v,w) '&' (Al,x,v,l3) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like non empty V24((Al,x)) quasi_total boolean-valued Element of K24(K25((Al,x),BOOLEAN))
In (((Al,x,v,w) '&' (Al,x,v,l3)),(Funcs ((Al,x),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,x),BOOLEAN)
x is Element of bound_QC-variables Al
All (x,w) is Element of CQC-WFF Al
(Al,x,v,(All (x,w))) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,x,(Al,x,v,w)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
In ((Al,x,x,(Al,x,v,w)),(Funcs ((Al,x),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,x),BOOLEAN)
y is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
y -ary_QC-pred_symbols Al is non empty Element of K24(())
K24(()) is set

q is Element of y -ary_QC-pred_symbols Al
q ! p is Element of CQC-WFF Al
(Al,x,v,(q ! p)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,y,y,q) is Element of relations_on x
(Al,x,y,p,(Al,x,y,y,q)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
v is Relation-like CQC-WFF Al -defined Funcs ((Al,x),BOOLEAN) -valued Function-like non empty V24( CQC-WFF Al) quasi_total Element of K24(K25((CQC-WFF Al),(Funcs ((Al,x),BOOLEAN))))
(Al,x,v,J) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,v,(VERUM Al)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
w is Element of CQC-WFF Al
'not' w is Element of CQC-WFF Al
(Al,x,v,()) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,v,w) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
'not' (Al,x,v,w) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like non empty V24((Al,x)) quasi_total boolean-valued Element of K24(K25((Al,x),BOOLEAN))
l3 is Element of CQC-WFF Al
w '&' l3 is Element of CQC-WFF Al
(Al,x,v,(w '&' l3)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,v,l3) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,v,w) '&' (Al,x,v,l3) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like non empty V24((Al,x)) quasi_total boolean-valued Element of K24(K25((Al,x),BOOLEAN))
x is Element of bound_QC-variables Al
All (x,w) is Element of CQC-WFF Al
(Al,x,v,(All (x,w))) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,x,(Al,x,v,w)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
y is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
y -ary_QC-pred_symbols Al is non empty Element of K24(())
K24(()) is set

q is Element of y -ary_QC-pred_symbols Al
q ! p is Element of CQC-WFF Al
(Al,x,v,(q ! p)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,y,y,q) is Element of relations_on x
(Al,x,y,p,(Al,x,y,y,q)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
In (('not' (Al,x,v,w)),(Funcs ((Al,x),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,x),BOOLEAN)
In (((Al,x,v,w) '&' (Al,x,v,l3)),(Funcs ((Al,x),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,x),BOOLEAN)
In ((Al,x,x,(Al,x,v,w)),(Funcs ((Al,x),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,x),BOOLEAN)
J is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
J -ary_QC-pred_symbols Al is non empty Element of K24(())
K24(()) is set
v is Element of J -ary_QC-pred_symbols Al

v ! s is Element of CQC-WFF Al
(Al,x,y,(v ! s)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,J,y,v) is Element of relations_on x
(Al,x,J,s,(Al,x,J,y,v)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
J is Element of CQC-WFF Al
(Al,x,y,J) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
'not' H5(J) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like non empty V24((Al,x)) quasi_total boolean-valued Element of K24(K25((Al,x),BOOLEAN))
'not' J is Element of CQC-WFF Al
(Al,x,y,()) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
In (('not' H5(J)),(Funcs ((Al,x),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,x),BOOLEAN)
J is Element of CQC-WFF Al
(Al,x,y,J) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
H5(A) '&' H5(J) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like non empty V24((Al,x)) quasi_total boolean-valued Element of K24(K25((Al,x),BOOLEAN))
A '&' J is Element of CQC-WFF Al
(Al,x,y,(A '&' J)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
In ((H5(A) '&' H5(J)),(Funcs ((Al,x),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,x),BOOLEAN)
J is Element of bound_QC-variables Al
All (J,A) is Element of CQC-WFF Al
(Al,x,y,(All (J,A))) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,J,(Al,x,y,A)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,J,H5(A)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
In ((Al,x,J,H5(A)),(Funcs ((Al,x),BOOLEAN))) is Relation-like Function-like Element of Funcs ((Al,x),BOOLEAN)

QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
Funcs ((),A) is functional 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 K24((QC-WFF Al))
K24((QC-WFF Al)) is set
(Al,A,x,(VERUM Al)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A) --> TRUE is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set

bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
QC-pred_symbols 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 K24((QC-WFF Al))
K24((QC-WFF Al)) is set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set
relations_on A is non empty set

(Al,A,y,(VERUM Al)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,y,(VERUM Al)) . x is boolean Element of BOOLEAN
(Al,A) --> TRUE is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set
((Al,A) --> TRUE) . x is boolean Element of BOOLEAN

bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
A is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
QC-pred_symbols Al is non empty set
x is non empty set
relations_on x is non empty set
A -ary_QC-pred_symbols Al is non empty Element of K24(())
K24(()) is set
(Al,x) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,x
Funcs ((),x) is functional non empty set

q is Element of A -ary_QC-pred_symbols Al

q ! y is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
(Al,x,p,(q ! y)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
Funcs ((Al,x),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,x), BOOLEAN
(Al,x,A,p,q) is Element of relations_on x
(Al,x,A,y,(Al,x,A,p,q)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)

bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
A -ary_QC-pred_symbols Al is non empty Element of K24(())
K24(()) is set
x is non empty set
(Al,x) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,x
Funcs ((),x) is functional non empty set
relations_on x is non empty set

(Al,x,A,p,y) is Relation-like NAT -defined x -valued Function-like FinSequence-like FinSequence of x
q is Element of CQC-WFF Al

(Al,x,J,q) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
Funcs ((Al,x),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,x), BOOLEAN
(Al,x,J,q) . y is boolean Element of BOOLEAN
s is Element of A -ary_QC-pred_symbols Al
s ! p is Element of CQC-WFF Al
(Al,x,A,J,s) is Element of relations_on x
v is Element of relations_on x
(Al,x,A,p,(Al,x,A,J,s)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,A,p,(Al,x,A,J,s)) . y is boolean Element of BOOLEAN

bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
A -ary_QC-pred_symbols Al is non empty Element of K24(())
K24(()) is set
x is non empty set
(Al,x) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,x
Funcs ((),x) is functional non empty set
relations_on x is non empty set

(Al,x,A,p,y) is Relation-like NAT -defined x -valued Function-like FinSequence-like FinSequence of x
q is Element of CQC-WFF Al

(Al,x,J,q) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
Funcs ((Al,x),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,x), BOOLEAN
(Al,x,J,q) . y is boolean Element of BOOLEAN
s is Element of A -ary_QC-pred_symbols Al
s ! p is Element of CQC-WFF Al
(Al,x,A,J,s) is Element of relations_on x
v is Element of relations_on x
(Al,x,A,p,(Al,x,A,J,s)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,A,p,(Al,x,A,J,s)) . y is boolean Element of BOOLEAN

QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
Funcs ((),A) is functional non empty set

x is Element of CQC-WFF Al
'not' x is Element of CQC-WFF Al
(Al,A,y,()) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,y,x) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
'not' (Al,A,y,x) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set

bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set
relations_on A is non empty set

y is Element of CQC-WFF Al
'not' y is Element of CQC-WFF Al

(Al,A,p,()) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,p,()) . x is boolean Element of BOOLEAN
(Al,A,p,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,y) . x is boolean Element of BOOLEAN
'not' ((Al,A,p,y) . x) is boolean Element of BOOLEAN
'not' (Al,A,p,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set
('not' (Al,A,p,y)) . x is boolean Element of BOOLEAN

QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
Funcs ((),A) is functional non empty set

x is Element of CQC-WFF Al
y is Element of CQC-WFF Al
x '&' y is Element of CQC-WFF Al
(Al,A,p,(x '&' y)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,p,x) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,x) '&' (Al,A,p,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set

bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set
relations_on A is non empty set

y is Element of CQC-WFF Al
p is Element of CQC-WFF Al
y '&' p is Element of CQC-WFF Al

(Al,A,q,(y '&' p)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,q,(y '&' p)) . x is boolean Element of BOOLEAN
(Al,A,q,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,y) . x is boolean Element of BOOLEAN
(Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,p) . x is boolean Element of BOOLEAN
((Al,A,q,y) . x) '&' ((Al,A,q,p) . x) is boolean Element of BOOLEAN
(Al,A,q,y) '&' (Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set
((Al,A,q,y) '&' (Al,A,q,p)) . x is boolean Element of BOOLEAN

QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24(())
K24(()) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set

x is Element of bound_QC-variables Al
y is Element of CQC-WFF Al
All (x,y) is Element of CQC-WFF Al
(Al,A,p,(All (x,y))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,p,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,(Al,A,p,y)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)

bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set
relations_on A is non empty set

y is Element of CQC-WFF Al
'not' y is Element of CQC-WFF Al
y '&' () is Element of CQC-WFF Al

(Al,A,p,(y '&' ())) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,p,(y '&' ())) . x is boolean Element of BOOLEAN
(Al,A,p,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,y) . x is boolean Element of BOOLEAN
'not' ((Al,A,p,y) . x) is boolean Element of BOOLEAN
((Al,A,p,y) . x) '&' ('not' ((Al,A,p,y) . x)) is boolean Element of BOOLEAN
(Al,A,p,()) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,()) . x is boolean Element of BOOLEAN
((Al,A,p,y) . x) '&' ((Al,A,p,()) . x) is boolean Element of BOOLEAN

bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set
relations_on A is non empty set

y is Element of CQC-WFF Al
'not' y is Element of CQC-WFF Al
y '&' () is Element of CQC-WFF Al
'not' (y '&' ()) is Element of CQC-WFF Al

(Al,A,p,('not' (y '&' ()))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,p,('not' (y '&' ()))) . x is boolean Element of BOOLEAN
(Al,A,p,(y '&' ())) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,(y '&' ())) . x is boolean Element of BOOLEAN
'not' ((Al,A,p,(y '&' ())) . x) is boolean Element of BOOLEAN

QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set

bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
QC-pred_symbols Al is non empty set
A is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
A -ary_QC-pred_symbols Al is non empty Element of K24(())
K24(()) is set
x is non empty set
(Al,x) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,x
Funcs ((),x) is functional non empty set
relations_on x is non empty set

J is Element of A -ary_QC-pred_symbols Al
J ! p is Element of CQC-WFF Al
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
(Al,x,A,q,J) is Element of relations_on x
(Al,x,A,p,(Al,x,A,q,J)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
Funcs ((Al,x),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,x), BOOLEAN
(Al,x,A,p,(Al,x,A,q,J)) . y is boolean Element of BOOLEAN
(Al,x,q,(J ! p)) is Relation-like (Al,x) -defined BOOLEAN -valued Function-like V24((Al,x)) quasi_total Element of Funcs ((Al,x),BOOLEAN)
(Al,x,q,(J ! p)) . y is boolean Element of BOOLEAN

bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set
relations_on A is non empty set

y is Element of CQC-WFF Al
'not' y is Element of CQC-WFF Al

(Al,A,p,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,p,y) . x is boolean Element of BOOLEAN
'not' ((Al,A,p,y) . x) is boolean Element of BOOLEAN
'not' (Al,A,p,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set
('not' (Al,A,p,y)) . x is boolean Element of BOOLEAN
(Al,A,p,()) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,p,()) . x is boolean Element of BOOLEAN

bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set
relations_on A is non empty set

y is Element of CQC-WFF Al
p is Element of CQC-WFF Al
y '&' p is Element of CQC-WFF Al

(Al,A,q,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,q,y) . x is boolean Element of BOOLEAN
(Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,p) . x is boolean Element of BOOLEAN
((Al,A,q,y) . x) '&' ((Al,A,q,p) . x) is boolean Element of BOOLEAN
(Al,A,q,y) '&' (Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like non empty V24((Al,A)) quasi_total boolean-valued Element of K24(K25((Al,A),BOOLEAN))
K25((Al,A),BOOLEAN) is set
K24(K25((Al,A),BOOLEAN)) is set
((Al,A,q,y) '&' (Al,A,q,p)) . x is boolean Element of BOOLEAN
(Al,A,q,(y '&' p)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,(y '&' p)) . x is boolean Element of BOOLEAN

QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24(())
K24(()) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set
relations_on A is non empty set
x is Element of bound_QC-variables Al

p is Element of CQC-WFF Al
All (x,p) is Element of CQC-WFF Al

(Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,x,(Al,A,q,p)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,(Al,A,q,p)) . y is boolean Element of BOOLEAN
(Al,A,q,(All (x,p))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,(All (x,p))) . y is boolean Element of BOOLEAN

QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24(())
K24(()) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set
relations_on A is non empty set
x is Element of bound_QC-variables Al

p is Element of CQC-WFF Al
All (x,p) is Element of CQC-WFF Al

(Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,x,(Al,A,q,p)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,(Al,A,q,p)) . y is boolean Element of BOOLEAN

(Al,A,q,p) . J is boolean Element of BOOLEAN

QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
Funcs ((),A) is functional non empty set
x is Element of CQC-WFF Al
'not' x is Element of CQC-WFF Al
'not' () is Element of CQC-WFF Al

(Al,A,y,('not' ())) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,y,x) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)

(Al,A,y,('not' ())) . p is boolean Element of BOOLEAN
(Al,A,y,()) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,y,()) . p is boolean Element of BOOLEAN
'not' ((Al,A,y,()) . p) is boolean Element of BOOLEAN
(Al,A,y,x) . p is boolean Element of BOOLEAN
'not' ((Al,A,y,x) . p) is boolean Element of BOOLEAN
'not' ('not' ((Al,A,y,x) . p)) is boolean Element of BOOLEAN

QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
Funcs ((),A) is functional non empty set
x is Element of CQC-WFF Al
x '&' x is Element of CQC-WFF Al

(Al,A,y,(x '&' x)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,y,x) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)

(Al,A,y,(x '&' x)) . p is boolean Element of BOOLEAN
(Al,A,y,x) . p is boolean Element of BOOLEAN
((Al,A,y,x) . p) '&' ((Al,A,y,x) . p) is boolean Element of BOOLEAN

bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set
relations_on A is non empty set

y is Element of CQC-WFF Al
p is Element of CQC-WFF Al
y => p is Element of CQC-WFF Al

(Al,A,q,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,q,y) . x is boolean Element of BOOLEAN
(Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,p) . x is boolean Element of BOOLEAN
(Al,A,q,(y => p)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,(y => p)) . x is boolean Element of BOOLEAN
'not' p is Element of CQC-WFF Al
y '&' () is Element of CQC-WFF Al
'not' (y '&' ()) is Element of CQC-WFF Al
(Al,A,q,('not' (y '&' ()))) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,('not' (y '&' ()))) . x is boolean Element of BOOLEAN
(Al,A,q,(y '&' ())) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,(y '&' ())) . x is boolean Element of BOOLEAN
'not' ((Al,A,q,(y '&' ())) . x) is boolean Element of BOOLEAN
(Al,A,q,()) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,()) . x is boolean Element of BOOLEAN
((Al,A,q,y) . x) '&' ((Al,A,q,()) . x) is boolean Element of BOOLEAN
'not' ((Al,A,q,p) . x) is boolean Element of BOOLEAN
((Al,A,q,y) . x) '&' ('not' ((Al,A,q,p) . x)) is boolean Element of BOOLEAN

bound_QC-variables Al is non empty Element of K24(())
QC-variables Al is non empty set
K24(()) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set
relations_on A is non empty set

y is Element of CQC-WFF Al
p is Element of CQC-WFF Al
y => p is Element of CQC-WFF Al

(Al,A,q,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
(Al,A,q,y) . x is boolean Element of BOOLEAN
(Al,A,q,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,q,p) . x is boolean Element of BOOLEAN

QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24(())
K24(()) is set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
x is Element of bound_QC-variables Al

p is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,p) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
(Al,A,x,p) . y is boolean Element of BOOLEAN
p . y is boolean Element of BOOLEAN
q is Element of bound_QC-variables Al
y . q is Element of A

QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
Al is boolean Element of BOOLEAN

Al '&' () is boolean Element of BOOLEAN
'not' (Al '&' ()) is boolean Element of BOOLEAN

A '&' x is boolean Element of BOOLEAN
'not' (A '&' x) is boolean Element of BOOLEAN
Al '&' x is boolean Element of BOOLEAN
('not' (A '&' x)) '&' (Al '&' x) is boolean Element of BOOLEAN
('not' (Al '&' ())) '&' (('not' (A '&' x)) '&' (Al '&' x)) is boolean Element of BOOLEAN
'not' (('not' (Al '&' ())) '&' (('not' (A '&' x)) '&' (Al '&' x))) is boolean Element of BOOLEAN

QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24(())
K24(()) is set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set
x is Element of bound_QC-variables Al

y is Element of bound_QC-variables Al
q . y is Element of A
J is set
p . J is set
s is Element of bound_QC-variables Al
K25((),A) is set
K24(K25((),A)) is set

dom J is set
rng J is set

s . x is Element of A
v is Element of bound_QC-variables Al
s . v is Element of A
p . v is Element of A
w is Element of bound_QC-variables Al
v is Element of bound_QC-variables Al
s . v is Element of A
p . v is Element of A

QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24(())
K24(()) is set
A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set
x is Element of bound_QC-variables Al

y is Element of bound_QC-variables Al
q . y is Element of A

QC-variables Al is non empty set
bound_QC-variables Al is non empty Element of K24(())
K24(()) is set
QC-WFF Al is non empty set
CQC-WFF Al is non empty Element of K24((QC-WFF Al))
K24((QC-WFF Al)) is set
QC-pred_symbols Al is non empty set
A is non empty set
relations_on A is non empty set
(Al,A) is functional non empty FUNCTION_DOMAIN of bound_QC-variables Al,A
Funcs ((),A) is functional non empty set
x is Element of bound_QC-variables Al
y is Element of CQC-WFF Al
still_not-bound_in y is Element of K24(())
K24(()) is set

(Al,A,p,y) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)
Funcs ((Al,A),BOOLEAN) is functional non empty FUNCTION_DOMAIN of (Al,A), BOOLEAN
v is ext-real V4() V5() V6() V7() V8() V9() ordinal natural V40() V45() Element of NAT
v -ary_QC-pred_symbols Al is non empty Element of K24(())
K24(()) is set
VERUM Al is Element of CQC-WFF Al
still_not-bound_in (VERUM Al) is Element of K24(())
(Al,A,p,(VERUM Al)) is Relation-like (Al,A) -defined BOOLEAN -valued Function-like V24((Al,A)) quasi_total Element of Funcs ((Al,A),BOOLEAN)

(Al,A,p,(VERUM Al)) . x is boolean