take {0,1} ; :: thesis: ( not {0,1} is trivial & {0,1} is finite )
thus ( not {0,1} is trivial & {0,1} is finite ) by Th3; :: thesis: verum