let n be Element of NAT ; :: thesis: for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected holds
N-min (L~ (Cage C,n)) = (Cage C,n) /. 1
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( C is connected implies N-min (L~ (Cage C,n)) = (Cage C,n) /. 1 )
set f = Cage C,n;
assume A1: C is connected ; :: thesis: N-min (L~ (Cage C,n)) = (Cage C,n) /. 1
then A2: for k being Element of NAT st 1 <= k & k + 1 <= len (Cage C,n) holds
( left_cell (Cage C,n),k,(Gauge C,n) misses C & right_cell (Cage C,n),k,(Gauge C,n) meets C ) by Th33;
( Cage C,n is_sequence_on Gauge C,n & ex i being Element of NAT st
( 1 <= i & i + 1 <= len (Gauge C,n) & (Cage C,n) /. 1 = (Gauge C,n) * i,(width (Gauge C,n)) & (Cage C,n) /. 2 = (Gauge C,n) * (i + 1),(width (Gauge C,n)) & N-min C in cell (Gauge C,n),i,((width (Gauge C,n)) -' 1) & N-min C <> (Gauge C,n) * i,((width (Gauge C,n)) -' 1) ) ) by A1, Def1;
hence N-min (L~ (Cage C,n)) = (Cage C,n) /. 1 by A2, Th32; :: thesis: verum