let X be Ordinal; :: thesis: for A being finite Subset of X holds RelIncl X linearly_orders A
let A be finite Subset of X; :: thesis: RelIncl X linearly_orders A
set b = chi (A,X);
A1: support (chi (A,X)) c= A

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in support (chi (A,X)) or y in A )
assume A2: y in support (chi (A,X)) ; :: thesis: y in A
A3: (chi (A,X)) . y <> 0 by A2, PRE_POLY:def 7;
then y in dom (chi (A,X)) by FUNCT_1:def 2;
hence y in A by A3, FUNCT_3:def 3; :: thesis: verum

end;

A4: A c= support (chi (A,X))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in A or y in support (chi (A,X)) )
assume A5: y in A ; :: thesis: y in support (chi (A,X))
(chi (A,X)) . y = 1 by FUNCT_3:def 3, A5;
hence y in support (chi (A,X)) by PRE_POLY:def 7; :: thesis: verum

end;

reconsider b = chi (A,X) as bag of X by PRE_POLY:def 8, A1;
RelIncl X linearly_orders support b by PRE_POLY:82;
hence RelIncl X linearly_orders A by A4, A1, XBOOLE_0:def 10; :: thesis: verum