let g be V8() standard clockwise_oriented special_circular_sequence; :: thesis: N-bound (L~ g) = N-bound (RightComp g)

set A = (Cl (RightComp g)) \ (RightComp g);

A1: N-bound (Cl (RightComp g)) = upper_bound (proj2 .: (Cl (RightComp g))) by SPRECT_1:45;

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;

( proj2 .: (Cl (RightComp g)) = proj2 .: (L~ g) & N-bound A = upper_bound (proj2 .: A) ) by Th30, SPRECT_1:45;

hence N-bound (L~ g) = N-bound (RightComp g) by A2, A3, A1, TOPREAL6:87; :: thesis: verum

set A = (Cl (RightComp g)) \ (RightComp g);

A1: N-bound (Cl (RightComp g)) = upper_bound (proj2 .: (Cl (RightComp g))) by SPRECT_1:45;

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;

( proj2 .: (Cl (RightComp g)) = proj2 .: (L~ g) & N-bound A = upper_bound (proj2 .: A) ) by Th30, SPRECT_1:45;

hence N-bound (L~ g) = N-bound (RightComp g) by A2, A3, A1, TOPREAL6:87; :: thesis: verum