let i be object ; :: according to FINSET_1:def 5 :: thesis: ( not i in I or [|A,B|] . i is finite )
assume A1: i in I ; :: thesis: [|A,B|] . i is finite
[:(A . i),(B . i):] is finite ;
hence [|A,B|] . i is finite by A1, PBOOLE:def 16; :: thesis: verum