let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1
A1: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32;
then 1 < (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:69;
then 1 < (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, SPRECT_2:70, XXREAL_0:2;
then 1 < (E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, SPRECT_2:71, XXREAL_0:2;
then 1 < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, SPRECT_2:72, XXREAL_0:2;
then 1 < (S-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A1, SPRECT_2:73, XXREAL_0:2;
hence (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 by A1, SPRECT_2:74, XXREAL_0:2; :: thesis: verum