theorem :: JORDAN1A:30

for i, j being Nat
for D being non empty Subset of (TOP-REAL 2) st i <= j holds
len (Gauge (D,i)) <= len (Gauge (D,j))