let i, j be Nat; :: thesis: ex n being Nat st square-uparrow n c= [:(NAT \ (Segm i)),(NAT \ (Segm j)):]

reconsider n = max (i,j) as Element of NAT by ORDINAL1:def 12;

take n ; :: thesis: square-uparrow n c= [:(NAT \ (Segm i)),(NAT \ (Segm j)):]

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

assume A1: x in square-uparrow n ; :: thesis: x in [:(NAT \ (Segm i)),(NAT \ (Segm j)):]

then reconsider y = x as Element of [:NAT,NAT:] ;

consider n1, n2 being Nat such that

A2: y `1 = n1 and

A3: y `2 = n2 and

A4: n <= n1 and

A5: n <= n2 by A1, Def3;

A6: y is pair by Th4;

i <= n by XXREAL_0:25;

then A7: not n1 in Segm i by A4, XXREAL_0:2, NAT_1:44;

n1 in NAT by ORDINAL1:def 12;

then A8: n1 in NAT \ (Segm i) by A7, XBOOLE_0:def 5;

j <= n by XXREAL_0:25;

then A9: not n2 in Segm j by A5, XXREAL_0:2, NAT_1:44;

n2 in NAT by ORDINAL1:def 12;

then n2 in NAT \ (Segm j) by A9, XBOOLE_0:def 5;

hence x in [:(NAT \ (Segm i)),(NAT \ (Segm j)):] by A2, A3, A6, A8, ZFMISC_1:def 2; :: thesis: verum

reconsider n = max (i,j) as Element of NAT by ORDINAL1:def 12;

take n ; :: thesis: square-uparrow n c= [:(NAT \ (Segm i)),(NAT \ (Segm j)):]

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

assume A1: x in square-uparrow n ; :: thesis: x in [:(NAT \ (Segm i)),(NAT \ (Segm j)):]

then reconsider y = x as Element of [:NAT,NAT:] ;

consider n1, n2 being Nat such that

A2: y `1 = n1 and

A3: y `2 = n2 and

A4: n <= n1 and

A5: n <= n2 by A1, Def3;

A6: y is pair by Th4;

i <= n by XXREAL_0:25;

then A7: not n1 in Segm i by A4, XXREAL_0:2, NAT_1:44;

n1 in NAT by ORDINAL1:def 12;

then A8: n1 in NAT \ (Segm i) by A7, XBOOLE_0:def 5;

j <= n by XXREAL_0:25;

then A9: not n2 in Segm j by A5, XXREAL_0:2, NAT_1:44;

n2 in NAT by ORDINAL1:def 12;

then n2 in NAT \ (Segm j) by A9, XBOOLE_0:def 5;

hence x in [:(NAT \ (Segm i)),(NAT \ (Segm j)):] by A2, A3, A6, A8, ZFMISC_1:def 2; :: thesis: verum