theorem :: GOBRD14:11

for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for r, t being Real st r > 0 & t > 0 holds
ex n being Nat st
( 1 < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t )