let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: (Gauge C,1) * (Center (Gauge C,1)),(len (Gauge C,1)) = |[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]|
set G = Gauge C,1;
1 <= len (Gauge C,1) by GOBRD11:34;
then A1: ((Gauge C,1) * (Center (Gauge C,1)),(len (Gauge C,1))) `1 = ((W-bound C) + (E-bound C)) / 2 by JORDAN1A:59;
1 <= Center (Gauge C,1) by Th12;
then ((Gauge C,1) * (Center (Gauge C,1)),(len (Gauge C,1))) `2 = N-bound (L~ (Cage C,1)) by Th14, JORDAN1A:91;
hence (Gauge C,1) * (Center (Gauge C,1)),(len (Gauge C,1)) = |[(((W-bound C) + (E-bound C)) / 2),(N-bound (L~ (Cage C,1)))]| by A1, EUCLID:57; :: thesis: verum