thus
( P is being_special_polygon implies ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P )
( ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P implies P is special_polygonal )proof
given p1,
p2 being
Point of
(TOP-REAL 2),
P1,
P2 being
Subset of
(TOP-REAL 2) such that A1:
p1 <> p2
and
p1 in P
and
p2 in P
and A2:
P1 is_S-P_arc_joining p1,
p2
and A3:
P2 is_S-P_arc_joining p1,
p2
and A4:
P1 /\ P2 = {p1,p2}
and A5:
P = P1 \/ P2
;
TOPREAL4:def 2 ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P
take
p1
;
ex p2 being Point of (TOP-REAL 2) st p1,p2 split P
take
p2
;
p1,p2 split P
thus
p1 <> p2
by A1;
SPPOL_2:def 1 ex f1, f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) )
consider f1 being
FinSequence of
(TOP-REAL 2) such that A6:
f1 is
being_S-Seq
and A7:
P1 = L~ f1
and A8:
p1 = f1 /. 1
and A9:
p2 = f1 /. (len f1)
by A2;
consider f2 being
FinSequence of
(TOP-REAL 2) such that A10:
f2 is
being_S-Seq
and A11:
P2 = L~ f2
and A12:
p1 = f2 /. 1
and A13:
p2 = f2 /. (len f2)
by A3;
reconsider f1 =
f1,
f2 =
f2 as
S-Sequence_in_R2 by A6, A10;
take
f1
;
ex f2 being S-Sequence_in_R2 st
( p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) )
take
f2
;
( p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) )
thus
(
p1 = f1 /. 1 &
p1 = f2 /. 1 &
p2 = f1 /. (len f1) &
p2 = f2 /. (len f2) &
(L~ f1) /\ (L~ f2) = {p1,p2} &
P = (L~ f1) \/ (L~ f2) )
by A4, A5, A7, A8, A9, A11, A12, A13;
verum
end;
given p1, p2 being Point of (TOP-REAL 2) such that A14:
p1,p2 split P
; P is special_polygonal
A15:
p2 in {p1,p2}
by TARSKI:def 2;
A16:
p1 in {p1,p2}
by TARSKI:def 2;
consider f1, f2 being S-Sequence_in_R2 such that
A17:
p1 = f1 /. 1
and
A18:
p1 = f2 /. 1
and
A19:
p2 = f1 /. (len f1)
and
A20:
p2 = f2 /. (len f2)
and
A21:
(L~ f1) /\ (L~ f2) = {p1,p2}
and
A22:
P = (L~ f1) \/ (L~ f2)
by A14;
take
p1
; TOPREAL4:def 2 ex b1 being Element of the carrier of (TOP-REAL 2) ex b2, b3 being Element of bool the carrier of (TOP-REAL 2) st
( not p1 = b1 & p1 in P & b1 in P & b2 is_S-P_arc_joining p1,b1 & b3 is_S-P_arc_joining p1,b1 & b2 /\ b3 = {p1,b1} & P = b2 \/ b3 )
take
p2
; ex b1, b2 being Element of bool the carrier of (TOP-REAL 2) st
( not p1 = p2 & p1 in P & p2 in P & b1 is_S-P_arc_joining p1,p2 & b2 is_S-P_arc_joining p1,p2 & b1 /\ b2 = {p1,p2} & P = b1 \/ b2 )
take P1 = L~ f1; ex b1 being Element of bool the carrier of (TOP-REAL 2) st
( not p1 = p2 & p1 in P & p2 in P & P1 is_S-P_arc_joining p1,p2 & b1 is_S-P_arc_joining p1,p2 & P1 /\ b1 = {p1,p2} & P = P1 \/ b1 )
take P2 = L~ f2; ( not p1 = p2 & p1 in P & p2 in P & P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
thus
p1 <> p2
by A14; ( p1 in P & p2 in P & P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
{p1,p2} c= P
by A21, A22, XBOOLE_1:29;
hence
( p1 in P & p2 in P )
by A16, A15; ( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
thus
ex f being FinSequence of (TOP-REAL 2) st
( f is being_S-Seq & P1 = L~ f & p1 = f /. 1 & p2 = f /. (len f) )
by A17, A19; TOPREAL4:def 1 ( P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
thus
ex f being FinSequence of (TOP-REAL 2) st
( f is being_S-Seq & P2 = L~ f & p1 = f /. 1 & p2 = f /. (len f) )
by A18, A20; TOPREAL4:def 1 ( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
thus
( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )
by A21, A22; verum