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
proof
( 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;
hence ex n being Nat st A c= square-downarrow n ; :: thesis: verum