let n be Nat; :: thesis: square-uparrow n = [:(NAT \ (Segm n)),(NAT \ (Segm n)):]
reconsider no = n as Element of OrderedNAT by ORDINAL1:def 12;
uparrow no = NAT \ (Segm n) by Th13;
hence square-uparrow n = [:(NAT \ (Segm n)),(NAT \ (Segm n)):] by Th26; :: thesis: verum