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 )
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:46, SPRECT_2:50;
assume A2: C is connected ; :: thesis: GoB (Cage C,n) = Gauge C,n
then 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 JORDAN1D:34;
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:43;
consider ie being Element of 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:29;
A8: 1 <= len (Gauge C,n) by GOBRD11:34;
then A9: [(len (Gauge C,n)),ie] in Indices (Gauge C,n) by A6, MATRIX_1:37;
consider iS being Element of 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:32;
A12: 1 <= width (Gauge C,n) by GOBRD11:34;
then A13: [iS,1] in Indices (Gauge C,n) by A10, MATRIX_1:37;
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 A2, JORDAN1D:25;
A16: [IN,(width (Gauge C,n))] in Indices (Gauge C,n) by A12, A14, MATRIX_1:37;
[1,iw] in Indices (Gauge C,n) by A8, A3, MATRIX_1:37;
hence GoB (Cage C,n) = Gauge C,n by A4, A11, A13, A7, A9, A1, A15, A16, A5, Th40, SPRECT_2:47; :: thesis: verum