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