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, Lm66, 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