let n be Ordinal; :: thesis: for b being bag of n holds RelIncl n linearly_orders support b
let b be bag of n; :: thesis: RelIncl n linearly_orders support b
set R = RelIncl n;
set s = support b;
for x, y being object 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 object ; :: thesis: ( x in support b & y in support b & x <> y & not [x,y] in RelIncl n implies [y,x] in RelIncl n )
assume that
A1: x in support b and
A2: y in support b and
x <> y ; :: thesis: ( [x,y] in RelIncl n or [y,x] in RelIncl n )
assume A3: not [x,y] in RelIncl n ; :: thesis: [y,x] in RelIncl n
reconsider x = x, y = y as Ordinal by A1, A2;
y c= x by A1, A2, A3, WELLORD2:def 1;
hence [y,x] in RelIncl n by A1, A2, WELLORD2:def 1; :: thesis: verum

end;

then A4: RelIncl n is_connected_in support b ;
A5: RelIncl n is_antisymmetric_in support b by Lm8;
A6: RelIncl n is_transitive_in support b by Lm8;
RelIncl n is_reflexive_in support b by Lm8;
hence RelIncl n linearly_orders support b by A4, A5, A6, ORDERS_1:def 9; :: thesis: verum