let n be Element of 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 )
assume A1: C is connected ; :: thesis: GoB (Cage C,n) = Gauge C,n
A2: ( 1 <= len (Gauge C,n) & 1 <= width (Gauge C,n) ) by GOBRD11:34;
consider iw being Element of 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 A1, JORDAN1D:34;
A5: [1,iw] in Indices (Gauge C,n) by A2, A3, MATRIX_1:37;
consider iS being Element of NAT such that
A6: ( 1 <= iS & iS <= len (Gauge C,n) ) and
A7: (Gauge C,n) * iS,1 = S-max (L~ (Cage C,n)) by A1, JORDAN1D:32;
A8: [iS,1] in Indices (Gauge C,n) by A2, A6, MATRIX_1:37;
A9: S-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:46;
consider ie being Element of NAT such that
A10: ( 1 <= ie & ie <= width (Gauge C,n) ) and
A11: (Gauge C,n) * (len (Gauge C,n)),ie = E-max (L~ (Cage C,n)) by A1, JORDAN1D:29;
A12: [(len (Gauge C,n)),ie] in Indices (Gauge C,n) by A2, A10, MATRIX_1:37;
A13: E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
consider IN being Element of 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 A1, JORDAN1D:25;
A16: [IN,(width (Gauge C,n))] in Indices (Gauge C,n) by A2, A14, MATRIX_1:37;
A17: N-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:43;
Cage C,n is_sequence_on Gauge C,n by A1, JORDAN9:def 1;
hence GoB (Cage C,n) = Gauge C,n by A4, A5, A7, A8, A9, A11, A12, A13, A15, A16, A17, Th40, SPRECT_2:47; :: thesis: verum