let X, Y be Subset of NAT; :: thesis: ( ( for n being Nat holds
( n in X iff 0 < n ) ) & ( for n being Nat holds
( n in Y iff 0 < n ) ) implies X = Y )
assume that
A2: for n being Nat holds
( n in X iff 0 < n ) and
A3: for n being Nat holds
( n in Y iff 0 < n ) ; :: thesis: X = Y
thus X c= Y by A2, A3; :: according to XBOOLE_0:def 10 :: thesis: Y c= X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in X )
assume A4: x in Y ; :: thesis: x in X
then reconsider x = x as Nat ;
0 < x by A3, A4;
hence x in X by A2; :: thesis: verum