set BO = BagOrder n;
BagOrder n linearly_orders Bags n by Lm4;
then ( field (BagOrder n) = Bags n & BagOrder n is_connected_in Bags n ) by ORDERS_1:15, ORDERS_1:def 9;
then BagOrder n is connected ;
hence BagOrder n is being_linear-order by ORDERS_1:def 6; :: thesis: verum