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