defpred S₁[ bag of I, bag of I] means ( $1 <> $2 & $1 divides $2 );
consider R being Relation of (Bags I) such that
A1: for b1, b2 being Element of Bags I holds
( [b1,b2] in R iff S₁[b1,b2] ) from RELSET_1:sch 2();
take R ; :: thesis: for b1, b2 being bag of I holds
( [b1,b2] in R iff ( b1 <> b2 & b1 divides b2 ) )
let b1, b2 be bag of I; :: thesis: ( [b1,b2] in R iff ( b1 <> b2 & b1 divides b2 ) )
( b1 in Bags I & b2 in Bags I ) by PRE_POLY:def 12;
hence ( [b1,b2] in R iff ( b1 <> b2 & b1 divides b2 ) ) by A1; :: thesis: verum