let n be Ordinal; :: thesis: for b, b1 being bag of n holds
( b1 in rng (divisors b) iff b1 divides b )
let b, b1 be bag of n; :: 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 and
A2: for p being bag of n holds
( p in S iff p divides b ) by PRE_POLY:def 16;
field (BagOrder n) = Bags n by ORDERS_1:100;
then A3: 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, A3, PRE_POLY:def 2;
hence b1 divides b by A2; :: thesis: verum

end;

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