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:38;

1 <= Center (Gauge (C,1)) by Th11;

then ((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))) `2 = N-bound (L~ (Cage (C,1))) by Th13, JORDAN1A:70;

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:53; :: thesis: verum

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:38;

1 <= Center (Gauge (C,1)) by Th11;

then ((Gauge (C,1)) * ((Center (Gauge (C,1))),(len (Gauge (C,1))))) `2 = N-bound (L~ (Cage (C,1))) by Th13, JORDAN1A:70;

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:53; :: thesis: verum