let i, j be Nat; :: thesis: for b being bag of j st i <= j holds
b | i is Element of Bags i
let b be bag of j; :: thesis: ( i <= j implies b | i is Element of Bags i )
assume A1: i <= j ; :: thesis: b | i is Element of Bags i
Segm i c= Segm j

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Segm i or x in Segm j )
assume x in Segm i ; :: thesis: x in Segm j
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: verum

end;

hence b | i is Element of Bags i by PRE_POLY:def 12; :: thesis: verum