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