now :: thesis: for i being object st i in I holds
not [|A,B|] . i is empty
let i be object ; :: thesis: ( i in I implies not [|A,B|] . i is empty )
assume A1: i in I ; :: thesis: not [|A,B|] . i is empty
then [|A,B|] . i = [:(A . i),(B . i):] by PBOOLE:def 16;
hence not [|A,B|] . i is empty by A1, ZFMISC_1:90; :: thesis: verum
end;
hence [|A,B|] is non-empty ; :: thesis: verum