set BO = BagOrder n;
A1: field (BagOrder n) = Bags n by ORDERS_1:100;
BagOrder n linearly_orders Bags n by Lm4;
then BagOrder n is_connected_in Bags n by ORDERS_1:def 8;
then BagOrder n is connected by A1, RELAT_2:def 14;
hence BagOrder n is being_linear-order by ORDERS_1:def 5; :: thesis: verum