:: deftheorem Def1 defines Involved HEYTING2:def 1 :
for V being set
for C being finite set
for A being Element of Fin (PFuncs (V,C))
for b₄ being set holds
( b₄ = Involved A iff for x being object holds
( x in b₄ iff ex f being finite Function st
( f in A & x in dom f ) ) );