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):]

now :: thesis: for x being object st x in [:(Segm i),(Segm j):] holds
x 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;

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