let A, B be Subset of NAT ; :: thesis: ( ( for n being Nat holds
( n in A iff n is prime ) ) & ( for n being Nat holds
( n in B iff n is prime ) ) implies A = B )
assume that
A3: for n being Nat holds
( n in A iff n is prime ) and
A4: for n being Nat holds
( n in B iff n is prime ) ; :: thesis: A = B
thus A c= B :: according to XBOOLE_0:def 10 :: thesis: B c= A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B )
assume A5: x in A ; :: thesis: x in B
then reconsider x = x as Element of NAT ;
x is prime by A3, A5;
hence x in B by A4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in A )
assume A6: x in B ; :: thesis: x in A
then reconsider x = x as Element of NAT ;
x is prime by A4, A6;
hence x in A by A3; :: thesis: verum