let g be constant standard clockwise_oriented special_circular_sequence; :: thesis: E-bound (L~ g) = E-bound (RightComp g)
set A = (Cl (RightComp g)) \ (RightComp g);
A1: E-bound (Cl (RightComp g)) = upper_bound (proj1 .: (Cl (RightComp g))) by SPRECT_1:46;
A2: L~ g = (Cl (RightComp g)) \ (RightComp g) by Th19;
Cl (RightComp g) is compact by Th32;
then A3: RightComp g is bounded by PRE_TOPC:18, RLTOPSP1:42;
reconsider A = (Cl (RightComp g)) \ (RightComp g) as non empty Subset of (TOP-REAL 2) by A2;
( proj1 .: (Cl (RightComp g)) = proj1 .: (L~ g) & E-bound A = upper_bound (proj1 .: A) ) by Th29, SPRECT_1:46;
hence E-bound (L~ g) = E-bound (RightComp g) by A2, A3, A1, TOPREAL6:86; :: thesis: verum