let n be Ordinal; :: thesis: BagOrder n linearly_orders Bags n
set BO = BagOrder n;
A1: BagOrder n is_transitive_in Bags n by Lm3;
A2: BagOrder n is_connected_in Bags n

proof

let x, y be object ; :: according to RELAT_2:def 6 :: thesis: ( not x in Bags n or not y in Bags n or x = y or [x,y] in BagOrder n or [y,x] in BagOrder n )
assume that
A3: ( x in Bags n & y in Bags n ) and
x <> y and
A4: not [x,y] in BagOrder n ; :: thesis: [y,x] in BagOrder n
reconsider p = x, q = y as bag of n by A3;
not p <=' q by A4, Def13;
then q <=' p by Th44;
hence [y,x] in BagOrder n by Def13; :: thesis: verum

end;

( BagOrder n is_reflexive_in Bags n & BagOrder n is_antisymmetric_in Bags n ) by Lm1, Lm2;
hence BagOrder n linearly_orders Bags n by A1, A2, ORDERS_1:def 9; :: thesis: verum