let n be Ordinal; :: thesis: BagOrder n linearly_orders Bags n
BagOrder n linearly_orders field (BagOrder n) by ORDERS_1:37;
hence BagOrder n linearly_orders Bags n by ORDERS_1:12; :: thesis: verum