consider a1, a2 being object such that
A1: ( a1 in X & a2 in X & a1 <> a2 ) by ZFMISC_1:def 10;
reconsider A = {a1,a2} as Subset of X by A1, ZFMISC_1:32;
take A ; :: thesis: ( A is finite & not A is trivial )
thus A is finite ; :: thesis: not A is trivial
( a1 in A & a2 in A ) by TARSKI:def 2;
hence not A is trivial by A1, ZFMISC_1:def 10; :: thesis: verum