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