let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); (Gauge (C,1)) * ((Center (Gauge (C,1))),1) = |[(((W-bound C) + (E-bound C)) / 2),(S-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))),1)) `1 = ((W-bound C) + (E-bound C)) / 2
by JORDAN1A:38;
Center (Gauge (C,1)) <= len (Gauge (C,1))
by Th13;
then
((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `2 = S-bound (L~ (Cage (C,1)))
by Th11, JORDAN1A:72;
hence
(Gauge (C,1)) * ((Center (Gauge (C,1))),1) = |[(((W-bound C) + (E-bound C)) / 2),(S-bound (L~ (Cage (C,1))))]|
by A1, EUCLID:53; verum