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

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

hence
b | i is Element of Bags i
by PRE_POLY:def 12; :: thesis: verum
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;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