let b1, b2 be bag of 1; :: thesis: ( ( b2 in rng (divisors b1) implies b2 . 0 <= b1 . 0 ) & ( b2 . 0 <= b1 . 0 implies b2 in rng (divisors b1) ) & ( b2 in rng (divisors b1) implies b2 divides b1 ) & ( b2 divides b1 implies b2 in rng (divisors b1) ) )
consider S being non empty finite Subset of (Bags 1) such that
A1: ( divisors b1 = SgmX ((BagOrder 1),S) & ( for p being bag of 1 holds
( p in S iff p divides b1 ) ) ) by PRE_POLY:def 16;
A2: BagOrder 1 linearly_orders S by Th9, ORDERS_1:38;
A3: ( b2 in rng (divisors b1) implies b2 . 0 <= b1 . 0 )

proof

assume b2 in rng (divisors b1) ; :: thesis: b2 . 0 <= b1 . 0
then b2 in S by A1, A2, PRE_POLY:def 2;
hence b2 . 0 <= b1 . 0 by A1, PRE_POLY:def 11; :: thesis: verum

end;

( b2 . 0 <= b1 . 0 implies b2 in rng (divisors b1) )

proof

assume b2 . 0 <= b1 . 0 ; :: thesis: b2 in rng (divisors b1)
then b2 in S by A1, Th8;
hence b2 in rng (divisors b1) by A1, A2, PRE_POLY:def 2; :: thesis: verum

end;

hence ( ( b2 in rng (divisors b1) implies b2 . 0 <= b1 . 0 ) & ( b2 . 0 <= b1 . 0 implies b2 in rng (divisors b1) ) & ( b2 in rng (divisors b1) implies b2 divides b1 ) & ( b2 divides b1 implies b2 in rng (divisors b1) ) ) by A3, Th8; :: thesis: verum