let A, P be Subset of (TOP-REAL 2); :: thesis: ( P is compact & |[(- 1),0]|,|[1,0]| realize-max-dist-in P & A is_inside_component_of P implies A c= closed_inside_of_rectangle ((- 1),1,(- 3),3) )
assume that
A1: P is compact and
A2: |[(- 1),0]|,|[1,0]| realize-max-dist-in P and
A3: A is_inside_component_of P ; :: thesis: A c= closed_inside_of_rectangle ((- 1),1,(- 3),3)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in closed_inside_of_rectangle ((- 1),1,(- 3),3) )
assume that
A4: x in A and
A5: not x in closed_inside_of_rectangle ((- 1),1,(- 3),3) ; :: thesis: contradiction
P c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A2, Th71;
then A6: (closed_inside_of_rectangle ((- 1),1,(- 3),3)) ` c= P ` by SUBSET_1:12;
reconsider x = x as Point of (TOP-REAL 2) by A4;
A7: ( not - 1 <= x `1 or not x `1 <= 1 or not - 3 <= x `2 or not x `2 <= 3 ) by A5;

per cases ( 0 <= x `1 or x `1 < 0 ) ;

suppose A8: 0 <= x `1 ; :: thesis: contradiction

set E = east_halfline x;
east_halfline x c= (closed_inside_of_rectangle ((- 1),1,(- 3),3)) `

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in east_halfline x or e in (closed_inside_of_rectangle ((- 1),1,(- 3),3)) ` )
assume A9: e in east_halfline x ; :: thesis: e in (closed_inside_of_rectangle ((- 1),1,(- 3),3)) `
then reconsider e = e as Point of (TOP-REAL 2) ;
A10: e `1 >= x `1 by A9, TOPREAL1:def 11;

now :: thesis: not e in closed_inside_of_rectangle ((- 1),1,(- 3),3)

assume e in closed_inside_of_rectangle ((- 1),1,(- 3),3) ; :: thesis: contradiction
then ex p being Point of (TOP-REAL 2) st
( e = p & - 1 <= p `1 & p `1 <= 1 & - 3 <= p `2 & p `2 <= 3 ) ;
hence contradiction by A7, A8, A9, A10, TOPREAL1:def 11, XXREAL_0:2; :: thesis: verum

end;

hence e in (closed_inside_of_rectangle ((- 1),1,(- 3),3)) ` by SUBSET_1:29; :: thesis: verum

end;

then east_halfline x c= P ` by A6;
then east_halfline x misses P by SUBSET_1:23;
then A11: east_halfline x c= UBD P by A1, JORDAN2C:127;
x in east_halfline x by TOPREAL1:38;
then A meets UBD P by A4, A11, XBOOLE_0:3;
hence contradiction by A3, Th14; :: thesis: verum

end;

suppose A12: x `1 < 0 ; :: thesis: contradiction

set E = west_halfline x;
west_halfline x c= (closed_inside_of_rectangle ((- 1),1,(- 3),3)) `

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in west_halfline x or e in (closed_inside_of_rectangle ((- 1),1,(- 3),3)) ` )
assume A13: e in west_halfline x ; :: thesis: e in (closed_inside_of_rectangle ((- 1),1,(- 3),3)) `
then reconsider e = e as Point of (TOP-REAL 2) ;
A14: e `1 <= x `1 by A13, TOPREAL1:def 13;

now :: thesis: not e in closed_inside_of_rectangle ((- 1),1,(- 3),3)

assume e in closed_inside_of_rectangle ((- 1),1,(- 3),3) ; :: thesis: contradiction
then ex p being Point of (TOP-REAL 2) st
( e = p & - 1 <= p `1 & p `1 <= 1 & - 3 <= p `2 & p `2 <= 3 ) ;
hence contradiction by A7, A12, A13, A14, TOPREAL1:def 13, XXREAL_0:2; :: thesis: verum

end;

hence e in (closed_inside_of_rectangle ((- 1),1,(- 3),3)) ` by SUBSET_1:29; :: thesis: verum

end;

then west_halfline x c= P ` by A6;
then west_halfline x misses P by SUBSET_1:23;
then A15: west_halfline x c= UBD P by A1, JORDAN2C:126;
x in west_halfline x by TOPREAL1:38;
then A meets UBD P by A4, A15, XBOOLE_0:3;
hence contradiction by A3, Th14; :: thesis: verum

end;

end;