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:100, ORDERS_1:def 8;
then BagOrder n is connected by RELAT_2:def 14;
hence BagOrder n is being_linear-order by ORDERS_1:def 5; :: thesis: verum