let n be Ordinal; :: thesis: for b being bag of holds RelIncl n linearly_orders support b
let b be bag of ; :: thesis: RelIncl n linearly_orders support b
set R = RelIncl n;
set s = support b;
for x, y being set st x in support b & y in support b & x <> y & not [x,y] in RelIncl n holds
[y,x] in RelIncl n

proof

let x, y be set ; :: thesis: ( x in support b & y in support b & x <> y & not [x,y] in RelIncl n implies [y,x] in RelIncl n )
assume A1: ( x in support b & y in support b & x <> y ) ; :: thesis: ( [x,y] in RelIncl n or [y,x] in RelIncl n )
assume A2: not [x,y] in RelIncl n ; :: thesis: [y,x] in RelIncl n
reconsider x = x, y = y as Ordinal by A1;
y c= x by A1, A2, WELLORD2:def 1;
hence [y,x] in RelIncl n by A1, WELLORD2:def 1; :: thesis: verum

end;

then A3: RelIncl n is_connected_in support b by RELAT_2:def 6;
( RelIncl n is_reflexive_in support b & RelIncl n is_antisymmetric_in support b & RelIncl n is_transitive_in support b ) by Lm1;
hence RelIncl n linearly_orders support b by A3, ORDERS_1:def 8; :: thesis: verum