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 by A3, A4; :: according to XBOOLE_0:def 10 :: thesis: B c= A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in A )
assume A5: x in B ; :: thesis: x in A
then reconsider x = x as Element of NAT ;
x is prime by A4, A5;
hence x in A by A3; :: thesis: verum