let F be Field; :: thesis: for S1 being non empty finite Subset of F
for p being Ppoly of F,S1
for q being non constant monic Polynomial of F holds
( q divides p iff ex S2 being non empty finite Subset of F st
( q is Ppoly of F,S2 & S2 c= S1 ) )
let S1 be non empty finite Subset of F; :: thesis: for p being Ppoly of F,S1
for q being non constant monic Polynomial of F holds
( q divides p iff ex S2 being non empty finite Subset of F st
( q is Ppoly of F,S2 & S2 c= S1 ) )
let p be Ppoly of F,S1; :: thesis: for q being non constant monic Polynomial of F holds
( q divides p iff ex S2 being non empty finite Subset of F st
( q is Ppoly of F,S2 & S2 c= S1 ) )
let q be non constant monic Polynomial of F; :: thesis: ( q divides p iff ex S2 being non empty finite Subset of F st
( q is Ppoly of F,S2 & S2 c= S1 ) )

now :: thesis: ( q divides p implies ex S2 being non empty finite Subset of F st
( q is Ppoly of F,S2 & S2 c= S1 ) )

assume q divides p ; :: thesis: ex S2 being non empty finite Subset of F st
( q is Ppoly of F,S2 & S2 c= S1 )
then consider B2 being non zero bag of the carrier of F such that
B: ( q is Ppoly of F,B2 & B2 divides Bag S1 ) by ppolydiv;
consider S2 being non empty finite Subset of F such that
C: ( B2 = Bag S2 & S2 c= S1 ) by B, bagset2;
thus ex S2 being non empty finite Subset of F st
( q is Ppoly of F,S2 & S2 c= S1 ) by B, C; :: thesis: verum

end;

hence ( q divides p iff ex S2 being non empty finite Subset of F st
( q is Ppoly of F,S2 & S2 c= S1 ) ) by ppolydiv, bagset1; :: thesis: verum