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