let i, j, k, l be Nat; :: thesis: ( i <= k & j <= l implies [:(Segm i),(Segm j):] c= [:(Segm k),(Segm l):] )

assume that

A1: i <= k and

A2: j <= l ; :: thesis: [:(Segm i),(Segm j):] c= [:(Segm k),(Segm l):]

assume that

A1: i <= k and

A2: j <= l ; :: thesis: [:(Segm i),(Segm j):] c= [:(Segm k),(Segm l):]

now :: thesis: for x being object st x in [:(Segm i),(Segm j):] holds

x in [:(Segm k),(Segm l):]

hence
[:(Segm i),(Segm j):] c= [:(Segm k),(Segm l):]
; :: thesis: verumx in [:(Segm k),(Segm l):]

let x be object ; :: thesis: ( x in [:(Segm i),(Segm j):] implies x in [:(Segm k),(Segm l):] )

assume x in [:(Segm i),(Segm j):] ; :: thesis: x in [:(Segm k),(Segm l):]

then consider xi, xj being object such that

A3: xi in Segm i and

A4: xj in Segm j and

A5: x = [xi,xj] by ZFMISC_1:def 2;

reconsider xi = xi, xj = xj as Nat by A3, A4;

( xi < k & xj < l ) by A1, A2, A3, A4, NAT_1:44, XXREAL_0:2;

then ( xi in Segm k & xj in Segm l ) by NAT_1:44;

hence x in [:(Segm k),(Segm l):] by A5, ZFMISC_1:def 2; :: thesis: verum

end;assume x in [:(Segm i),(Segm j):] ; :: thesis: x in [:(Segm k),(Segm l):]

then consider xi, xj being object such that

A3: xi in Segm i and

A4: xj in Segm j and

A5: x = [xi,xj] by ZFMISC_1:def 2;

reconsider xi = xi, xj = xj as Nat by A3, A4;

( xi < k & xj < l ) by A1, A2, A3, A4, NAT_1:44, XXREAL_0:2;

then ( xi in Segm k & xj in Segm l ) by NAT_1:44;

hence x in [:(Segm k),(Segm l):] by A5, ZFMISC_1:def 2; :: thesis: verum