let x be Element of N; :: thesis: x is Element of S
thus x is Element of S ; :: thesis: verum