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

proof

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

end;

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