let A be finite Subset of [:NAT,NAT:]; ex m, n being Nat st A c= [:(Segm m),(Segm n):]
per cases
( A is empty or not A is empty )
;
suppose A1:
not
A is
empty
;
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
{ x where x is Element of NAT : ex y being Element of NAT st [x,y] in A } c= NAT
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
{ y where y is Element of NAT : ex x being Element of NAT st [x,y] in A } c= NAT
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 ;
TARSKI:def 3 ( not t in A or t in [:(Segm (x1 + 1)),(Segm (y1 + 1)):] )
assume A12:
t in A
;
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;
verum
end; hence
ex
m,
n being
Nat st
A c= [:(Segm m),(Segm n):]
;
verum end; end;