take 4 ; :: thesis: 4 is composite
thus 4 is composite by INT_2:29; :: thesis: verum