let n be Nat; for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected holds
GoB (Cage (C,n)) = Gauge (C,n)
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ( C is connected implies GoB (Cage (C,n)) = Gauge (C,n) )
A1:
( S-max (L~ (Cage (C,n))) in rng (Cage (C,n)) & E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) )
by SPRECT_2:42, SPRECT_2:46;
assume A2:
C is connected
; GoB (Cage (C,n)) = Gauge (C,n)
then consider iw being Nat such that
A3:
( 1 <= iw & iw <= width (Gauge (C,n)) )
and
A4:
W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (1,iw)
by JORDAN1D:30;
A5:
( N-min (L~ (Cage (C,n))) in rng (Cage (C,n)) & Cage (C,n) is_sequence_on Gauge (C,n) )
by A2, JORDAN9:def 1, SPRECT_2:39;
consider ie being Nat such that
A6:
( 1 <= ie & ie <= width (Gauge (C,n)) )
and
A7:
(Gauge (C,n)) * ((len (Gauge (C,n))),ie) = E-max (L~ (Cage (C,n)))
by A2, JORDAN1D:25;
A8:
1 <= len (Gauge (C,n))
by GOBRD11:34;
then A9:
[(len (Gauge (C,n))),ie] in Indices (Gauge (C,n))
by A6, MATRIX_0:30;
consider iS being Nat such that
A10:
( 1 <= iS & iS <= len (Gauge (C,n)) )
and
A11:
(Gauge (C,n)) * (iS,1) = S-max (L~ (Cage (C,n)))
by A2, JORDAN1D:28;
A12:
1 <= width (Gauge (C,n))
by GOBRD11:34;
then A13:
[iS,1] in Indices (Gauge (C,n))
by A10, MATRIX_0:30;
consider IN being Nat such that
A14:
( 1 <= IN & IN <= len (Gauge (C,n)) )
and
A15:
(Gauge (C,n)) * (IN,(width (Gauge (C,n)))) = N-min (L~ (Cage (C,n)))
by A2, JORDAN1D:21;
A16:
[IN,(width (Gauge (C,n)))] in Indices (Gauge (C,n))
by A12, A14, MATRIX_0:30;
[1,iw] in Indices (Gauge (C,n))
by A8, A3, MATRIX_0:30;
hence
GoB (Cage (C,n)) = Gauge (C,n)
by A4, A11, A13, A7, A9, A1, A15, A16, A5, Th34, SPRECT_2:43; verum