let x be set ; :: according to MEMBERED:def 5 :: thesis: ( x in INT implies x is integer )
thus ( x in INT implies x is integer ) ; :: thesis: verum