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

proof

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

end;

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