let i, j be Nat; :: thesis:
let b be bag of j; :: thesis:
assume A1: i <= j ; :: thesis:
Segm i c= Segm j

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Segm i ; :: thesis:
then x in { y where y is Nat : y < i } by AXIOMS:4;
then consider x9 being Nat such that
A2: x9 = x and
A3: x9 < i ;
x9 < j by A1, A3, XXREAL_0:2;
then x9 in { y where y is Nat : y < j } ;
hence x in Segm j by A2, AXIOMS:4; :: thesis:

end;