let X be natural-membered set ; :: thesis: ( ( for n being natural number holds n in X ) implies X = NAT )
assume A1: for n being natural number holds n in X ; :: thesis: X = NAT
thus X c= NAT by Th6; :: according to XBOOLE_0:def 10 :: thesis: NAT c= X
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in NAT or e in X )
assume e in NAT ; :: thesis: e in X
then e is natural ;
hence e in X by A1; :: thesis: verum