{ i where i is Element of I : b1 . i <> b2 . i } c= I

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { i where i is Element of I : b1 . i <> b2 . i } or a in I )
assume a in { i where i is Element of I : b1 . i <> b2 . i } ; :: thesis: a in I
then ex i being Element of I st
( a = i & b1 . i <> b2 . i ) ;
hence a in I ; :: thesis: verum

end;

then reconsider F = { i where i is Element of I : b1 . i <> b2 . i } as finite set by FINSET_1:13;
card F = card F ;
hence card { i where i is Element of I : b1 . i <> b2 . i } is Nat ; :: thesis: verum