let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( C is connected implies for n being Nat holds N-min (L~ (Cage (C,n))) = (Cage (C,n)) /. 1 )
assume A1: C is connected ; :: thesis: for n being Nat holds N-min (L~ (Cage (C,n))) = (Cage (C,n)) /. 1
let n be Nat; :: thesis: N-min (L~ (Cage (C,n))) = (Cage (C,n)) /. 1
set f = Cage (C,n);
A2: for k being 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 A1, Th31;
( Cage (C,n) is_sequence_on Gauge (C,n) & ex i being 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, Th30; :: thesis: verum