A1: { n where n is Nat : card (primeNumbers (n,100)) = 25 } c= {0,2,3,4,9,10}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { n where n is Nat : card (primeNumbers (n,100)) = 25 } or x in {0,2,3,4,9,10} )
assume x in { n where n is Nat : card (primeNumbers (n,100)) = 25 } ; :: thesis: x in {0,2,3,4,9,10}
then consider n being Nat such that
A2: ( x = n & card (primeNumbers (n,100)) = 25 ) ;
n < 10 + 1 by A2, Th96;
then n <= 10 by NAT_1:13;
then not not n = 0 & ... & not n = 10 ;
hence x in {0,2,3,4,9,10} by A2, Th85, ENUMSET1:def 4; :: thesis: verum

end;

{0,2,3,4,9,10} c= { n where n is Nat : card (primeNumbers (n,100)) = 25 }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {0,2,3,4,9,10} or x in { n where n is Nat : card (primeNumbers (n,100)) = 25 } )
assume A3: x in {0,2,3,4,9,10} ; :: thesis: x in { n where n is Nat : card (primeNumbers (n,100)) = 25 }
then reconsider n = x as Nat ;
( n = 0 or n = 2 or n = 3 or n = 4 or n = 9 or n = 10 ) by A3, ENUMSET1:def 4;
then card (primeNumbers (n,100)) = 25 by Th85;
hence x in { n where n is Nat : card (primeNumbers (n,100)) = 25 } ; :: thesis: verum

end;

hence { n where n is Nat : card (primeNumbers (n,100)) = 25 } = {0,2,3,4,9,10} by A1, XBOOLE_0:def 10; :: thesis: verum