let i be Nat; :: thesis: for x being object st x in i holds
x is Element of NAT
let x be object ; :: thesis: ( x in i implies x is Element of NAT )
i c= NAT ;
hence ( x in i implies x is Element of NAT ) ; :: thesis: verum