A1: NATPLUS c= NAT \ {0}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NATPLUS or x in NAT \ {0} )
assume A2: x in NATPLUS ; :: thesis: x in NAT \ {0}
then reconsider x = x as Element of NAT ;
not x in {0} by A2, TARSKI:def 1;
hence x in NAT \ {0} by XBOOLE_0:def 5; :: thesis: verum

end;

NAT \ {0} c= NATPLUS

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NAT \ {0} or x in NATPLUS )
assume A3: x in NAT \ {0} ; :: thesis: x in NATPLUS
then reconsider x = x as Element of NAT ;
not x in {0} by A3, XBOOLE_0:def 5;
then x <> 0 by TARSKI:def 1;
hence x in NATPLUS by NAT_LAT:def 6; :: thesis: verum

end;

hence NATPLUS = NAT \ {0} by A1, XBOOLE_0:def 10; :: thesis: verum