let C be Simple_closed_curve; :: thesis: ( |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in C implies LSeg |[1,(- 3)]|,|[0 ,(- 3)]| misses C )
assume |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in C ; :: thesis: LSeg |[1,(- 3)]|,|[0 ,(- 3)]| misses C
then A1: C /\ (rectangle (- 1),1,(- 3),3) = {|[(- 1),0 ]|,|[1,0 ]|} by Th74;
assume LSeg |[1,(- 3)]|,|[0 ,(- 3)]| meets C ; :: thesis: contradiction
then consider q being set such that
A2: q in LSeg |[1,(- 3)]|,|[0 ,(- 3)]| and
A3: q in C by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A3;
q in (rectangle (- 1),1,(- 3),3) /\ C by A2, A3, Lm69, XBOOLE_0:def 4;
then ( q = |[(- 1),0 ]| or q = |[1,0 ]| ) by A1, TARSKI:def 2;
hence contradiction by A2, Lm20, Lm21, TOPREAL3:18; :: thesis: verum