let i, j, k, l be Nat; ( i <= k & j <= l implies [:(Segm i),(Segm j):] c= [:(Segm k),(Segm l):] )
assume that
A1:
i <= k
and
A2:
j <= l
; [:(Segm i),(Segm j):] c= [:(Segm k),(Segm l):]
now for x being object st x in [:(Segm i),(Segm j):] holds
x in [:(Segm k),(Segm l):]let x be
object ;
( x in [:(Segm i),(Segm j):] implies x in [:(Segm k),(Segm l):] )assume
x in [:(Segm i),(Segm j):]
;
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;
verum end;
hence
[:(Segm i),(Segm j):] c= [:(Segm k),(Segm l):]
; verum