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