let g be non constant standard clockwise_oriented special_circular_sequence; :: thesis: S-bound (L~ g) = S-bound (RightComp g)
set A = (Cl (RightComp g)) \ (RightComp g);
A1: L~ g = (Cl (RightComp g)) \ (RightComp g) by Th29;
then reconsider A = (Cl (RightComp g)) \ (RightComp g) as non empty Subset of (TOP-REAL 2) ;
A2: proj2 .: (Cl (RightComp g)) = proj2 .: (L~ g) by Th40;
Cl (RightComp g) is compact by Th42;
then ( RightComp g c= Cl (RightComp g) & Cl (RightComp g) is Bounded ) by PRE_TOPC:48;
then A3: RightComp g is Bounded by JORDAN2C:16;
( S-bound A = lower_bound (proj2 .: A) & S-bound (Cl (RightComp g)) = lower_bound (proj2 .: (Cl (RightComp g))) ) by SPRECT_1:49;
hence S-bound (L~ g) = S-bound (RightComp g) by A1, A2, A3, TOPREAL6:97; :: thesis: verum