let a, b, c, d be Real; for p1, p2 being Point of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st a < b & c < d & p1 in closed_inside_of_rectangle (a,b,c,d) & not p2 in closed_inside_of_rectangle (a,b,c,d) & P is_an_arc_of p1,p2 holds
Segment (P,p1,p2,p1,(First_Point (P,p1,p2,(rectangle (a,b,c,d))))) c= closed_inside_of_rectangle (a,b,c,d)
let p1, p2 be Point of (TOP-REAL 2); for P being Subset of (TOP-REAL 2) st a < b & c < d & p1 in closed_inside_of_rectangle (a,b,c,d) & not p2 in closed_inside_of_rectangle (a,b,c,d) & P is_an_arc_of p1,p2 holds
Segment (P,p1,p2,p1,(First_Point (P,p1,p2,(rectangle (a,b,c,d))))) c= closed_inside_of_rectangle (a,b,c,d)
let P be Subset of (TOP-REAL 2); ( a < b & c < d & p1 in closed_inside_of_rectangle (a,b,c,d) & not p2 in closed_inside_of_rectangle (a,b,c,d) & P is_an_arc_of p1,p2 implies Segment (P,p1,p2,p1,(First_Point (P,p1,p2,(rectangle (a,b,c,d))))) c= closed_inside_of_rectangle (a,b,c,d) )
set R = closed_inside_of_rectangle (a,b,c,d);
set dR = rectangle (a,b,c,d);
set n = First_Point (P,p1,p2,(rectangle (a,b,c,d)));
assume that
A1:
a < b
and
A2:
c < d
and
A3:
p1 in closed_inside_of_rectangle (a,b,c,d)
and
A4:
not p2 in closed_inside_of_rectangle (a,b,c,d)
and
A5:
P is_an_arc_of p1,p2
; Segment (P,p1,p2,p1,(First_Point (P,p1,p2,(rectangle (a,b,c,d))))) c= closed_inside_of_rectangle (a,b,c,d)
let x be object ; TARSKI:def 3 ( not x in Segment (P,p1,p2,p1,(First_Point (P,p1,p2,(rectangle (a,b,c,d))))) or x in closed_inside_of_rectangle (a,b,c,d) )
assume that
A6:
x in Segment (P,p1,p2,p1,(First_Point (P,p1,p2,(rectangle (a,b,c,d)))))
and
A7:
not x in closed_inside_of_rectangle (a,b,c,d)
; contradiction
reconsider x = x as Point of (TOP-REAL 2) by A6;
A8:
Fr (closed_inside_of_rectangle (a,b,c,d)) = rectangle (a,b,c,d)
by A1, A2, Th52;
p1 in P
by A5, TOPREAL1:1;
then A9:
P meets closed_inside_of_rectangle (a,b,c,d)
by A3, XBOOLE_0:3;
p2 in P
by A5, TOPREAL1:1;
then
P \ (closed_inside_of_rectangle (a,b,c,d)) <> {} (TOP-REAL 2)
by A4, XBOOLE_0:def 5;
then A10:
P meets rectangle (a,b,c,d)
by A5, A8, A9, CONNSP_1:22, JORDAN6:10;
A11:
P is closed
by A5, JORDAN6:11;
then A12:
P /\ (rectangle (a,b,c,d)) is closed
;
A13:
First_Point (P,p1,p2,(rectangle (a,b,c,d))) in P /\ (rectangle (a,b,c,d))
by A5, A10, A11, JORDAN5C:def 1;
per cases
( x = First_Point (P,p1,p2,(rectangle (a,b,c,d))) or x <> First_Point (P,p1,p2,(rectangle (a,b,c,d))) )
;
suppose
x = First_Point (
P,
p1,
p2,
(rectangle (a,b,c,d)))
;
contradictionthen A14:
x in rectangle (
a,
b,
c,
d)
by A13, XBOOLE_0:def 4;
rectangle (
a,
b,
c,
d)
c= closed_inside_of_rectangle (
a,
b,
c,
d)
by A1, A2, Th45;
hence
contradiction
by A7, A14;
verum end; suppose A15:
x <> First_Point (
P,
p1,
p2,
(rectangle (a,b,c,d)))
;
contradictionreconsider P =
P as non
empty Subset of
(TOP-REAL 2) by A5, TOPREAL1:1;
consider f being
Function of
I[01],
((TOP-REAL 2) | P) such that A16:
f is
being_homeomorphism
and A17:
f . 0 = p1
and A18:
f . 1
= p2
by A5, TOPREAL1:def 1;
A19:
rng f =
[#] ((TOP-REAL 2) | P)
by A16, TOPS_2:def 5
.=
P
by PRE_TOPC:def 5
;
First_Point (
P,
p1,
p2,
(rectangle (a,b,c,d)))
in P
by A13, XBOOLE_0:def 4;
then consider na being
object such that A20:
na in dom f
and A21:
f . na = First_Point (
P,
p1,
p2,
(rectangle (a,b,c,d)))
by A19, FUNCT_1:def 3;
reconsider na =
na as
Real by A20;
A22:
0 <= na
by A20, BORSUK_1:43;
A23:
na <= 1
by A20, BORSUK_1:43;
A24:
Segment (
P,
p1,
p2,
p1,
(First_Point (P,p1,p2,(rectangle (a,b,c,d)))))
c= P
by JORDAN16:2;
then consider xa being
object such that A25:
xa in dom f
and A26:
f . xa = x
by A6, A19, FUNCT_1:def 3;
reconsider xa =
xa as
Real by A25;
A27:
0 <= xa
by A25, BORSUK_1:43;
A28:
xa <= 1
by A25, BORSUK_1:43;
A29:
Segment (
P,
p1,
p2,
p1,
x)
is_an_arc_of p1,
x
by A3, A5, A6, A7, A24, JORDAN16:24;
then
p1 in Segment (
P,
p1,
p2,
p1,
x)
by TOPREAL1:1;
then A30:
Segment (
P,
p1,
p2,
p1,
x)
meets closed_inside_of_rectangle (
a,
b,
c,
d)
by A3, XBOOLE_0:3;
x in Segment (
P,
p1,
p2,
p1,
x)
by A29, TOPREAL1:1;
then
(Segment (P,p1,p2,p1,x)) \ (closed_inside_of_rectangle (a,b,c,d)) <> {} (TOP-REAL 2)
by A7, XBOOLE_0:def 5;
then
Segment (
P,
p1,
p2,
p1,
x)
meets Fr (closed_inside_of_rectangle (a,b,c,d))
by A29, A30, CONNSP_1:22, JORDAN6:10;
then consider z being
object such that A31:
z in Segment (
P,
p1,
p2,
p1,
x)
and A32:
z in rectangle (
a,
b,
c,
d)
by A8, XBOOLE_0:3;
reconsider z =
z as
Point of
(TOP-REAL 2) by A31;
Segment (
P,
p1,
p2,
p1,
x)
= { p where p is Point of (TOP-REAL 2) : ( LE p1,p,P,p1,p2 & LE p,x,P,p1,p2 ) }
by JORDAN6:26;
then A33:
ex
zz being
Point of
(TOP-REAL 2) st
(
zz = z &
LE p1,
zz,
P,
p1,
p2 &
LE zz,
x,
P,
p1,
p2 )
by A31;
Segment (
P,
p1,
p2,
p1,
x)
c= P
by JORDAN16:2;
then consider za being
object such that A34:
za in dom f
and A35:
f . za = z
by A19, A31, FUNCT_1:def 3;
reconsider za =
za as
Real by A34;
A36:
0 <= za
by A34, BORSUK_1:43;
A37:
za <= 1
by A34, BORSUK_1:43;
A38:
na <= za
by A5, A10, A12, A16, A17, A18, A21, A23, A32, A35, A36, JORDAN5C:def 1;
A39:
za <= xa
by A16, A17, A18, A26, A27, A28, A33, A35, A37, JORDAN5C:def 3;
Segment (
P,
p1,
p2,
p1,
(First_Point (P,p1,p2,(rectangle (a,b,c,d)))))
= { p where p is Point of (TOP-REAL 2) : ( LE p1,p,P,p1,p2 & LE p, First_Point (P,p1,p2,(rectangle (a,b,c,d))),P,p1,p2 ) }
by JORDAN6:26;
then
ex
xx being
Point of
(TOP-REAL 2) st
(
xx = x &
LE p1,
xx,
P,
p1,
p2 &
LE xx,
First_Point (
P,
p1,
p2,
(rectangle (a,b,c,d))),
P,
p1,
p2 )
by A6;
then
xa <= na
by A16, A17, A18, A21, A22, A23, A26, A28, JORDAN5C:def 3;
then
xa < na
by A15, A21, A26, XXREAL_0:1;
hence
contradiction
by A38, A39, XXREAL_0:2;
verum end;