:: deftheorem defines Hall HALLMAR1:def 4 :
for F being finite set
for A being FinSequence of bool F holds
( A is Hall iff for J being finite set st J c= dom A holds
card J <= card (union (A,J)) );