let A be finite Subset of [:NAT,NAT:]; :: thesis: ex m, n being Nat st A c= [:(Segm m),(Segm n):]

per cases
( A is empty or not A is empty )
;

end;

suppose
A is empty
; :: thesis: ex m, n being Nat st A c= [:(Segm m),(Segm n):]

then
A c= [:(Segm 0),(Segm 0):]
;

hence ex m, n being Nat st A c= [:(Segm m),(Segm n):] ; :: thesis: verum

end;hence ex m, n being Nat st A c= [:(Segm m),(Segm n):] ; :: thesis: verum

suppose A1:
not A is empty
; :: thesis: ex m, n being Nat st A c= [:(Segm m),(Segm n):]

set A1 = { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } ;

A2: not { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } is empty

reconsider A = A as Relation ;

proj1 A is finite ;

then B1 is finite by Th14;

then sup B1 in { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } by XXREAL_2:def 6;

then consider x1 being Element of NAT such that

A6: sup B1 = x1 and

ex y being Element of NAT st [x1,y] in A ;

set A2 = { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } ;

A7: not { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } is empty

reconsider A = A as Relation ;

proj2 A is finite ;

then B2 is finite by Th15;

then sup B2 in { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } by XXREAL_2:def 6;

then consider y1 being Element of NAT such that

A11: sup B2 = y1 and

ex x being Element of NAT st [x,y1] in A ;

A c= [:(Segm (x1 + 1)),(Segm (y1 + 1)):]

end;A2: not { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } is empty

proof

{ x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } c= NAT
set n = the Element of A;

the Element of A in A by A1;

then consider x, y being object such that

A3: x in NAT and

A4: y in NAT and

A5: the Element of A = [x,y] by ZFMISC_1:def 2;

reconsider x = x, y = y as Element of NAT by A3, A4;

x in { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } by A4, A5, A1;

hence not { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } is empty ; :: thesis: verum

end;the Element of A in A by A1;

then consider x, y being object such that

A3: x in NAT and

A4: y in NAT and

A5: the Element of A = [x,y] by ZFMISC_1:def 2;

reconsider x = x, y = y as Element of NAT by A3, A4;

x in { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } by A4, A5, A1;

hence not { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } is empty ; :: thesis: verum

proof

then reconsider B1 = { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } as non empty ext-real-membered set by A2;
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } or t in NAT )

assume t in { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } ; :: thesis: t in NAT

then ex x being Element of NAT st

( t = x & ex y being Element of NAT st [x,y] in A ) ;

hence t in NAT ; :: thesis: verum

end;assume t in { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } ; :: thesis: t in NAT

then ex x being Element of NAT st

( t = x & ex y being Element of NAT st [x,y] in A ) ;

hence t in NAT ; :: thesis: verum

reconsider A = A as Relation ;

proj1 A is finite ;

then B1 is finite by Th14;

then sup B1 in { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } by XXREAL_2:def 6;

then consider x1 being Element of NAT such that

A6: sup B1 = x1 and

ex y being Element of NAT st [x1,y] in A ;

set A2 = { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } ;

A7: not { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } is empty

proof

{ y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } c= NAT
set n = the Element of A;

the Element of A in A by A1;

then consider x, y being object such that

A8: x in NAT and

A9: y in NAT and

A10: the Element of A = [x,y] by ZFMISC_1:def 2;

reconsider x = x, y = y as Element of NAT by A8, A9;

y in { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } by A8, A10, A1;

hence not { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } is empty ; :: thesis: verum

end;the Element of A in A by A1;

then consider x, y being object such that

A8: x in NAT and

A9: y in NAT and

A10: the Element of A = [x,y] by ZFMISC_1:def 2;

reconsider x = x, y = y as Element of NAT by A8, A9;

y in { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } by A8, A10, A1;

hence not { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } is empty ; :: thesis: verum

proof

then reconsider B2 = { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } as non empty ext-real-membered set by A7;
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } or t in NAT )

assume t in { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } ; :: thesis: t in NAT

then ex y being Element of NAT st

( t = y & ex x being Element of NAT st [x,y] in A ) ;

hence t in NAT ; :: thesis: verum

end;assume t in { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } ; :: thesis: t in NAT

then ex y being Element of NAT st

( t = y & ex x being Element of NAT st [x,y] in A ) ;

hence t in NAT ; :: thesis: verum

reconsider A = A as Relation ;

proj2 A is finite ;

then B2 is finite by Th15;

then sup B2 in { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } by XXREAL_2:def 6;

then consider y1 being Element of NAT such that

A11: sup B2 = y1 and

ex x being Element of NAT st [x,y1] in A ;

A c= [:(Segm (x1 + 1)),(Segm (y1 + 1)):]

proof

hence
ex m, n being Nat st A c= [:(Segm m),(Segm n):]
; :: thesis: verum
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in A or t in [:(Segm (x1 + 1)),(Segm (y1 + 1)):] )

assume A12: t in A ; :: thesis: t in [:(Segm (x1 + 1)),(Segm (y1 + 1)):]

then reconsider u = t as Element of [:NAT,NAT:] ;

consider x, y being object such that

A13: x in NAT and

A14: y in NAT and

A15: u = [x,y] by ZFMISC_1:def 2;

reconsider x2 = x, y2 = y as Element of NAT by A13, A14;

x2 in { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } by A12, A14, A15;

then x2 <= sup B1 by XXREAL_2:4;

then x2 < x1 + 1 by A6, NAT_1:13;

then A16: x2 in Segm (x1 + 1) by NAT_1:44;

y2 in { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } by A12, A13, A15;

then y2 <= sup B2 by XXREAL_2:4;

then y2 < y1 + 1 by A11, NAT_1:13;

then y2 in Segm (y1 + 1) by NAT_1:44;

hence t in [:(Segm (x1 + 1)),(Segm (y1 + 1)):] by A16, A15, ZFMISC_1:def 2; :: thesis: verum

end;assume A12: t in A ; :: thesis: t in [:(Segm (x1 + 1)),(Segm (y1 + 1)):]

then reconsider u = t as Element of [:NAT,NAT:] ;

consider x, y being object such that

A13: x in NAT and

A14: y in NAT and

A15: u = [x,y] by ZFMISC_1:def 2;

reconsider x2 = x, y2 = y as Element of NAT by A13, A14;

x2 in { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } by A12, A14, A15;

then x2 <= sup B1 by XXREAL_2:4;

then x2 < x1 + 1 by A6, NAT_1:13;

then A16: x2 in Segm (x1 + 1) by NAT_1:44;

y2 in { y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } by A12, A13, A15;

then y2 <= sup B2 by XXREAL_2:4;

then y2 < y1 + 1 by A11, NAT_1:13;

then y2 in Segm (y1 + 1) by NAT_1:44;

hence t in [:(Segm (x1 + 1)),(Segm (y1 + 1)):] by A16, A15, ZFMISC_1:def 2; :: thesis: verum