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} ; :: 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, A2, A3, Th3, ZFMISC_1:32; :: thesis: verum

A1: x in X and

A2: y in X and

A3: 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, A2, A3, Th3, ZFMISC_1:32; :: thesis: verum