let n be Ordinal; :: thesis: BagOrder n linearly_orders Bags n
set BO = BagOrder n;
A1: BagOrder n is_reflexive_in Bags n by Lm1;
A2: BagOrder n is_antisymmetric_in Bags n by Lm2;
A3: BagOrder n is_transitive_in Bags n by Lm3;
BagOrder n is_connected_in Bags n

proof

let x, y be set ; :: 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 A4: ( x in Bags n & y in Bags n & x <> y & not [x,y] in BagOrder n ) ; :: thesis: [y,x] in BagOrder n
then reconsider p = x, q = y as bag of by Def14;
not p <=' q by A4, Def16;
then q <=' p by Th49;
hence [y,x] in BagOrder n by Def16; :: thesis: verum

end;

hence BagOrder n linearly_orders Bags n by A1, A2, A3, ORDERS_1:def 8; :: thesis: verum