let p be Prime; :: thesis: for X being included_in_Seg set st X c= SetPrimes & p divides Product (Sgm X) holds
p in X
let X be included_in_Seg set ; :: thesis: ( X c= SetPrimes & p divides Product (Sgm X) implies p in X )
assume A1: X c= SetPrimes ; :: thesis: ( not p divides Product (Sgm X) or p in X )
A2: rng (Sgm X) = X by FINSEQ_1:def 14;
then Sgm X is FinSequence of SetPrimes by A1, FINSEQ_1:def 4;
hence ( not p divides Product (Sgm X) or p in X ) by A2, NAT_3:8; :: thesis: verum