let C be Simple_closed_curve; :: thesis: Lower_Middle_Point C in C
A1: Lower_Middle_Point C in Lower_Arc C by JORDAN6:81;
Lower_Arc C c= C by JORDAN6:76;
hence Lower_Middle_Point C in C by A1; :: thesis: verum