let n be Nat; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum