let B, A be set ; :: thesis: ( not B is finite implies not B in [:A,B:] )
assume that
Z1: not B is finite and
Z2: B in [:A,B:] ; :: thesis: contradiction
ex x being set st
( x in A & B = [x,{x}] ) by Z2, ZFMISC_1:154;
hence contradiction by Z1; :: thesis: verum