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