let S be non empty being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis: ( Lower_Arc S c= S & Upper_Arc S c= S )
S = (Lower_Arc S) \/ (Upper_Arc S) by Th50;
hence ( Lower_Arc S c= S & Upper_Arc S c= S ) by XBOOLE_1:7; :: thesis: verum