let n be Nat; :: thesis: square-downarrow n = [:(Segm n),(Segm n):]

thus square-downarrow n c= [:(Segm n),(Segm n):] :: according to XBOOLE_0:def 10 :: thesis: [:(Segm n),(Segm n):] c= square-downarrow n

assume x in [:(Segm n),(Segm n):] ; :: thesis: x in square-downarrow n

then consider y1, y2 being object such that

A9: y1 in Segm n and

A10: y2 in Segm n and

A11: x = [y1,y2] by ZFMISC_1:def 2;

reconsider y1 = y1, y2 = y2 as Nat by A9, A10;

A12: ( y1 = x `1 & y2 = x `2 & y1 < n & y2 < n ) by A11, A9, A10, NAT_1:44;

x is Element of [:NAT,NAT:] by A9, A10, A11, ZFMISC_1:def 2;

hence x in square-downarrow n by A12, Def4; :: thesis: verum

thus square-downarrow n c= [:(Segm n),(Segm n):] :: according to XBOOLE_0:def 10 :: thesis: [:(Segm n),(Segm n):] c= square-downarrow n

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:(Segm n),(Segm n):] or x in square-downarrow n )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in square-downarrow n or x in [:(Segm n),(Segm n):] )

assume A2: x in square-downarrow n ; :: thesis: x in [:(Segm n),(Segm n):]

then consider n1, n2 being Nat such that

A3: n1 = x `1 and

A4: n2 = x `2 and

A5: n1 < n and

A6: n2 < n by Def4;

A7: n1 in Segm n by A5, NAT_1:44;

A8: n2 in Segm n by A6, NAT_1:44;

ex x1, x2 being object st

( x1 in NAT & x2 in NAT & x = [x1,x2] ) by A2, ZFMISC_1:def 2;

then reconsider x = x as pair object ;

x = [n1,n2] by A3, A4;

hence x in [:(Segm n),(Segm n):] by A7, A8, ZFMISC_1:def 2; :: thesis: verum

end;assume A2: x in square-downarrow n ; :: thesis: x in [:(Segm n),(Segm n):]

then consider n1, n2 being Nat such that

A3: n1 = x `1 and

A4: n2 = x `2 and

A5: n1 < n and

A6: n2 < n by Def4;

A7: n1 in Segm n by A5, NAT_1:44;

A8: n2 in Segm n by A6, NAT_1:44;

ex x1, x2 being object st

( x1 in NAT & x2 in NAT & x = [x1,x2] ) by A2, ZFMISC_1:def 2;

then reconsider x = x as pair object ;

x = [n1,n2] by A3, A4;

hence x in [:(Segm n),(Segm n):] by A7, A8, ZFMISC_1:def 2; :: thesis: verum

assume x in [:(Segm n),(Segm n):] ; :: thesis: x in square-downarrow n

then consider y1, y2 being object such that

A9: y1 in Segm n and

A10: y2 in Segm n and

A11: x = [y1,y2] by ZFMISC_1:def 2;

reconsider y1 = y1, y2 = y2 as Nat by A9, A10;

A12: ( y1 = x `1 & y2 = x `2 & y1 < n & y2 < n ) by A11, A9, A10, NAT_1:44;

x is Element of [:NAT,NAT:] by A9, A10, A11, ZFMISC_1:def 2;

hence x in square-downarrow n by A12, Def4; :: thesis: verum