consider x, y being set such that
A1: ( x in X & y in X & x <> y ) by ZFMISC_1:def 10;
take {x,y} ; :: thesis: ( {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, Th4, ZFMISC_1:38; :: thesis: verum