let n be Ordinal; for b being bag of n holds RelIncl n linearly_orders support b
let b be bag of n; 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 ;
( 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
;
( [x,y] in RelIncl n or [y,x] in RelIncl n )
assume A3:
not
[x,y] in RelIncl n
;
[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;
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; verum