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

( 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