let f be Element of S; :: thesis: f is Element of P
thus f is Element of P ; :: thesis: verum