let F be finite set ; :: thesis: for A being non empty FinSequence of bool F st A is Hall holds
A is non-empty
let A be non empty FinSequence of bool F; :: thesis: ( A is Hall implies A is non-empty )
assume A1: A is Hall ; :: thesis: A is non-empty
assume not A is non-empty ; :: thesis: contradiction
then {} in rng A by RELAT_1:def 9;
then consider i being object such that
A2: ( i in dom A & A . i = {} ) by FUNCT_1:def 3;
set J = {i};
A3: card {i} = 1 by CARD_2:42;
( {i} c= dom A & card (union (A,{i})) = 0 ) by A2, Th5, CARD_1:27, ZFMISC_1:31;
hence contradiction by A1, A3; :: thesis: verum