let i be set ; :: according to FINSET_1:def 4 :: thesis: ( not i in I or (A \/ B) . i is finite )
assume A1: i in I ; :: thesis: (A \/ B) . i is finite
then ( A . i is finite & B . i is finite ) by LL1;
then (A . i) \/ (B . i) is finite ;
hence (A \/ B) . i is finite by A1, PBOOLE:def 7; :: thesis: verum