let A be finite Subset of [:NAT,NAT:]; :: thesis: ex n being Nat st A c= square-downarrow n

consider m, n being Nat such that

A1: A c= [:(Segm m),(Segm n):] by Th16;

reconsider m = m, n = n as Element of NAT by ORDINAL1:def 12;

reconsider mn = max (m,n) as Nat ;

A c= square-downarrow mn

consider m, n being Nat such that

A1: A c= [:(Segm m),(Segm n):] by Th16;

reconsider m = m, n = n as Element of NAT by ORDINAL1:def 12;

reconsider mn = max (m,n) as Nat ;

A c= square-downarrow mn

proof

hence
ex n being Nat st A c= square-downarrow n
; :: thesis: verum
( Segm m c= Segm mn & Segm n c= Segm mn )
by XXREAL_0:25, NAT_1:39;

then [:(Segm m),(Segm n):] c= [:(Segm mn),(Segm mn):] by ZFMISC_1:96;

then [:(Segm m),(Segm n):] c= square-downarrow mn by Th30;

hence A c= square-downarrow mn by A1; :: thesis: verum

end;then [:(Segm m),(Segm n):] c= [:(Segm mn),(Segm mn):] by ZFMISC_1:96;

then [:(Segm m),(Segm n):] c= square-downarrow mn by Th30;

hence A c= square-downarrow mn by A1; :: thesis: verum