let n be non zero Nat; :: thesis: for x being object st x in [:(bool (SetPrimes n)),(Seg n):] holds
x `1 is finite Subset of SetPrimes
let x be object ; :: thesis: ( x in [:(bool (SetPrimes n)),(Seg n):] implies x `1 is finite Subset of SetPrimes )
assume G1: x in [:(bool (SetPrimes n)),(Seg n):] ; :: thesis: x `1 is finite Subset of SetPrimes
x is pair by CARDFIL4:4, G1;
then x = [(x `1),(x `2)] ;
then reconsider g1 = x `1 as Subset of (SetPrimes n) by G1, ZFMISC_1:87;
SetPrimes n c= SetPrimes by XBOOLE_1:17;
then g1 c= SetPrimes ;
hence x `1 is finite Subset of SetPrimes ; :: thesis: verum