let n be Nat; 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); (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; verum