for F being non empty finite set
for A being non empty FinSequence of bool F holds
( ex X being set st X is_a_system_of_different_representatives_of A iff A is Hall )