let P be non empty Subset of (TOP-REAL 2); ( P is being_simple_closed_curve iff ex p1, p2 being Point of (TOP-REAL 2) ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) )
hereby ( ex p1, p2 being Point of (TOP-REAL 2) ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) implies P is being_simple_closed_curve )
assume A1:
P is
being_simple_closed_curve
;
ex p1, p2 being Point of (TOP-REAL 2) ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} )then consider p1,
p2 being
Point of
(TOP-REAL 2) such that A2:
p1 <> p2
and A3:
p1 in P
and A4:
p2 in P
by Th5;
consider P1,
P2 being non
empty Subset of
(TOP-REAL 2) such that A5:
P1 is_an_arc_of p1,
p2
and A6:
P2 is_an_arc_of p1,
p2
and A7:
P = P1 \/ P2
and A8:
P1 /\ P2 = {p1,p2}
by A1, A2, A3, A4, Th5;
take p1 =
p1;
ex p2 being Point of (TOP-REAL 2) ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} )take p2 =
p2;
ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} )take P1 =
P1;
ex P2 being non empty Subset of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} )take P2 =
P2;
( p1 <> p2 & p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} )thus
(
p1 <> p2 &
p1 in P &
p2 in P &
P1 is_an_arc_of p1,
p2 &
P2 is_an_arc_of p1,
p2 &
P = P1 \/ P2 &
P1 /\ P2 = {p1,p2} )
by A2, A3, A4, A5, A6, A7, A8;
verum
end;
thus
( ex p1, p2 being Point of (TOP-REAL 2) ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) implies P is being_simple_closed_curve )
by Lm34; verum