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 ) ;

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;

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

proof

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;

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

proof

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;

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;
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

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;

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

proof

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;

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;
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

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;

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

end;

end;