for F being non empty finite set
for A being non empty FinSequence of bool F st ( for i being Element of NAT st i in dom A holds
card (A . i) = 1 ) & A is Hall holds
ex X being set st X is_a_system_of_different_representatives_of A