let n be non zero Nat; :: thesis: for x being object st x in bool (SetPrimes n) holds
x is finite Subset of SetPrimes
let x be object ; :: thesis: ( x in bool (SetPrimes n) implies x is finite Subset of SetPrimes )
assume G1: x in bool (SetPrimes n) ; :: thesis: x is finite Subset of SetPrimes
reconsider g1 = x as Subset of (SetPrimes n) by G1;
SetPrimes n c= SetPrimes by XBOOLE_1:17;
then g1 c= SetPrimes ;
hence x is finite Subset of SetPrimes ; :: thesis: verum