let C be Simple_closed_curve; :: thesis: for A being non empty Subset of (TOP-REAL 2) st A is_an_arc_of W-min C, E-max C & A c= C & not A = Lower_Arc C holds
A = Upper_Arc C
let A be non empty Subset of (TOP-REAL 2); :: thesis: ( A is_an_arc_of W-min C, E-max C & A c= C & not A = Lower_Arc C implies A = Upper_Arc C )
assume that
A1: A is_an_arc_of W-min C, E-max C and
A2: A c= C ; :: thesis: ( A = Lower_Arc C or A = Upper_Arc C )
A is compact by A1, JORDAN5A:1;
hence ( A = Lower_Arc C or A = Upper_Arc C ) by A1, A2, TOPMETR3:15; :: thesis: verum