let C be Simple_closed_curve; :: thesis: Lower_Middle_Point C in C
( Lower_Middle_Point C in Lower_Arc C & Lower_Arc C c= C ) by JORDAN6:61, JORDAN6:66;
hence Lower_Middle_Point C in C ; :: thesis: verum