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 object 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, Lm74, XBOOLE_0:def 4;
then ( q = |[(- 1),0]| or q = |[1,0]| ) by A1, TARSKI:def 2;
hence contradiction by A2, Lm18, Lm19, TOPREAL3:12; :: thesis: verum