consider x, y being object such that
A1:
x in X
and
A2:
y in X
and
A3:
x <> y
by ZFMISC_1:def 10;
take
{x,y}
; ( {x,y} is Subset of X & not {x,y} is trivial & {x,y} is finite )
thus
( {x,y} is Subset of X & not {x,y} is trivial & {x,y} is finite )
by A1, A2, A3, Th3, ZFMISC_1:32; verum