thus {A} is non-empty :: thesis: {A} is finite-yielding

proof

let i be object ; :: according to PBOOLE:def 13 :: thesis: ( not i in I or not {A} . i is empty )
assume A1: i in I ; :: thesis: not {A} . i is empty
{(A . i)} <> {} ;
hence not {A} . i is empty by A1, Def1; :: thesis: verum

end;

let i be object ; :: according to FINSET_1:def 5 :: thesis: ( not i in I or {A} . i is finite )
assume A2: i in I ; :: thesis: {A} . i is finite
{(A . i)} is finite ;
hence {A} . i is finite by A2, Def1; :: thesis: verum