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 :: according to XBOOLE_0:def 10 :: thesis: Y c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Y )
assume A4: x in X ; :: thesis: x in Y
then reconsider x = x as Nat ;
0 < x by A2, A4;
hence x in Y by A3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in X )
assume A5: x in Y ; :: thesis: x in X
then reconsider x = x as Nat ;
0 < x by A3, A5;
hence x in X by A2; :: thesis: verum