let n be Ordinal; :: thesis: for b, b1 being bag of holds
( b1 in rng (divisors b) iff b1 divides b )
let b, b1 be bag of ; :: thesis: ( b1 in rng (divisors b) iff b1 divides b )
consider S being non empty finite Subset of (Bags n) such that
A1: ( divisors b = SgmX (BagOrder n),S & ( for p being bag of holds
( p in S iff p divides b ) ) ) by POLYNOM1:def 18;
field (BagOrder n) = Bags n by ORDERS_1:100;
then A2: BagOrder n linearly_orders S by ORDERS_1:133, ORDERS_1:134;

hereby :: thesis: ( b1 divides b implies b1 in rng (divisors b) )

assume b1 in rng (divisors b) ; :: thesis: b1 divides b
then b1 in S by A1, A2, TRIANG_1:def 2;
hence b1 divides b by A1; :: thesis: verum

end;

assume b1 divides b ; :: thesis: b1 in rng (divisors b)
then b1 in S by A1;
hence b1 in rng (divisors b) by A1, A2, TRIANG_1:def 2; :: thesis: verum