let a, b, c, d be real number ; :: thesis: 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); :: thesis: 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); :: thesis: ( 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 & c < d )
and
A2:
p1 in closed_inside_of_rectangle a,b,c,d
and
A3:
not p2 in closed_inside_of_rectangle a,b,c,d
and
A4:
P is_an_arc_of p1,p2
; :: thesis: 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 set ; :: according to TARSKI:def 3 :: thesis: ( 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
A5:
x in Segment P,p1,p2,p1,(First_Point P,p1,p2,(rectangle a,b,c,d))
and
A6:
not x in closed_inside_of_rectangle a,b,c,d
; :: thesis: contradiction
reconsider x = x as Point of (TOP-REAL 2) by A5;
A7:
Fr (closed_inside_of_rectangle a,b,c,d) = rectangle a,b,c,d
by A1, Th52;
p1 in P
by A4, TOPREAL1:4;
then A8:
P meets closed_inside_of_rectangle a,b,c,d
by A2, XBOOLE_0:3;
p2 in P
by A4, TOPREAL1:4;
then
P \ (closed_inside_of_rectangle a,b,c,d) <> {} (TOP-REAL 2)
by A3, XBOOLE_0:def 5;
then A9:
P meets rectangle a,b,c,d
by A4, A7, A8, CONNSP_1:23, JORDAN6:11;
P is closed
by A4, JORDAN6:12;
then A10:
P /\ (rectangle a,b,c,d) is closed
by TOPS_1:35;
then A11:
First_Point P,p1,p2,(rectangle a,b,c,d) in P /\ (rectangle a,b,c,d)
by A4, A9, 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)
;
:: thesis: contradictionthen A12:
x in rectangle a,
b,
c,
d
by A11, XBOOLE_0:def 4;
rectangle a,
b,
c,
d c= closed_inside_of_rectangle a,
b,
c,
d
by A1, Th45;
hence
contradiction
by A6, A12;
:: thesis: verum end; suppose A13:
x <> First_Point P,
p1,
p2,
(rectangle a,b,c,d)
;
:: thesis: contradictionreconsider P =
P as non
empty Subset of
(TOP-REAL 2) by A4, TOPREAL1:4;
consider f being
Function of
I[01] ,
((TOP-REAL 2) | P) such that A14:
f is
being_homeomorphism
and A15:
(
f . 0 = p1 &
f . 1
= p2 )
by A4, TOPREAL1:def 2;
A16:
rng f =
[#] ((TOP-REAL 2) | P)
by A14, TOPS_2:def 5
.=
P
by PRE_TOPC:def 10
;
First_Point P,
p1,
p2,
(rectangle a,b,c,d) in P
by A11, XBOOLE_0:def 4;
then consider na being
set such that A17:
na in dom f
and A18:
f . na = First_Point P,
p1,
p2,
(rectangle a,b,c,d)
by A16, FUNCT_1:def 5;
na is
real
by A17;
then reconsider na =
na as
Real by XREAL_0:def 1;
A19:
(
0 <= na &
na <= 1 )
by A17, BORSUK_1:86;
A20:
Segment P,
p1,
p2,
p1,
(First_Point P,p1,p2,(rectangle a,b,c,d)) c= P
by JORDAN16:5;
then consider xa being
set such that A21:
xa in dom f
and A22:
f . xa = x
by A5, A16, FUNCT_1:def 5;
xa is
real
by A21;
then reconsider xa =
xa as
Real by XREAL_0:def 1;
A23:
(
0 <= xa &
xa <= 1 )
by A21, BORSUK_1:86;
A24:
Segment P,
p1,
p2,
p1,
x is_an_arc_of p1,
x
by A2, A4, A5, A6, A20, JORDAN16:39;
then
p1 in Segment P,
p1,
p2,
p1,
x
by TOPREAL1:4;
then A25:
Segment P,
p1,
p2,
p1,
x meets closed_inside_of_rectangle a,
b,
c,
d
by A2, XBOOLE_0:3;
x in Segment P,
p1,
p2,
p1,
x
by A24, TOPREAL1:4;
then
(Segment P,p1,p2,p1,x) \ (closed_inside_of_rectangle a,b,c,d) <> {} (TOP-REAL 2)
by A6, XBOOLE_0:def 5;
then
Segment P,
p1,
p2,
p1,
x meets Fr (closed_inside_of_rectangle a,b,c,d)
by A24, A25, CONNSP_1:23, JORDAN6:11;
then consider z being
set such that A26:
z in Segment P,
p1,
p2,
p1,
x
and A27:
z in rectangle a,
b,
c,
d
by A7, XBOOLE_0:3;
reconsider z =
z as
Point of
(TOP-REAL 2) by A26;
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:29;
then consider zz being
Point of
(TOP-REAL 2) such that A28:
zz = z
and
LE p1,
zz,
P,
p1,
p2
and A29:
LE zz,
x,
P,
p1,
p2
by A26;
Segment P,
p1,
p2,
p1,
x c= P
by JORDAN16:5;
then consider za being
set such that A30:
za in dom f
and A31:
f . za = z
by A16, A26, FUNCT_1:def 5;
za is
real
by A30;
then reconsider za =
za as
Real by XREAL_0:def 1;
A32:
(
0 <= za &
za <= 1 )
by A30, BORSUK_1:86;
then A33:
na <= za
by A4, A9, A10, A14, A15, A18, A19, A27, A31, JORDAN5C:def 1;
A34:
za <= xa
by A14, A15, A22, A23, A28, A29, A31, A32, 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:29;
then consider xx being
Point of
(TOP-REAL 2) such that A35:
xx = x
and
LE p1,
xx,
P,
p1,
p2
and A36:
LE xx,
First_Point P,
p1,
p2,
(rectangle a,b,c,d),
P,
p1,
p2
by A5;
xa <= na
by A14, A15, A18, A19, A22, A23, A35, A36, JORDAN5C:def 3;
then
xa < na
by A13, A18, A22, XXREAL_0:1;
hence
contradiction
by A33, A34, XXREAL_0:2;
:: thesis: verum end;