let P, A 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 set ; :: 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:31;
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 set ; :: 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 & e `2 = x `2 ) by A9, TOPREAL1:def 13;

now

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, A10, XXREAL_0:2; :: thesis: verum

end;

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

end;

then east_halfline x c= P ` by A6, XBOOLE_1:1;
then east_halfline x misses P by SUBSET_1:43;
then A11: east_halfline x c= UBD P by A1, JORDAN2C:135;
x in east_halfline x by TOPREAL1:45;
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 set ; :: 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 & e `2 = x `2 ) by A13, TOPREAL1:def 15;

now

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, A14, XXREAL_0:2; :: thesis: verum

end;

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

end;

then west_halfline x c= P ` by A6, XBOOLE_1:1;
then west_halfline x misses P by SUBSET_1:43;
then A15: west_halfline x c= UBD P by A1, JORDAN2C:134;
x in west_halfline x by TOPREAL1:45;
then A meets UBD P by A4, A15, XBOOLE_0:3;
hence contradiction by A3, Th14; :: thesis: verum

end;

end;