for x being object
for n being Nat
for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T holds
( x in s .: (square-uparrow n) iff ex i, j being Nat st
( n <= i & n <= j & x = s . (i,j) ) )