let n be Nat; :: thesis: square-downarrow n is finite Subset of [:NAT,NAT:]
[:(Segm n),(Segm n):] is finite ;
hence square-downarrow n is finite Subset of [:NAT,NAT:] by Th30; :: thesis: verum