let A be Subset of (TOP-REAL 2); ( A ` <> {} implies ( ( A is boundary & A is Jordan ) iff ex A1, A2 being Subset of (TOP-REAL 2) st
( A ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A = (Cl A1) \ A1 & ( for C1, C2 being Subset of ((TOP-REAL 2) | (A `)) st C1 = A1 & C2 = A2 holds
( C1 is a_component & C2 is a_component ) ) ) ) )
assume A1:
A ` <> {}
; ( ( A is boundary & A is Jordan ) iff ex A1, A2 being Subset of (TOP-REAL 2) st
( A ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A = (Cl A1) \ A1 & ( for C1, C2 being Subset of ((TOP-REAL 2) | (A `)) st C1 = A1 & C2 = A2 holds
( C1 is a_component & C2 is a_component ) ) ) )
hereby ( ex A1, A2 being Subset of (TOP-REAL 2) st
( A ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A = (Cl A1) \ A1 & ( for C1, C2 being Subset of ((TOP-REAL 2) | (A `)) st C1 = A1 & C2 = A2 holds
( C1 is a_component & C2 is a_component ) ) ) implies ( A is boundary & A is Jordan ) )
assume that A2:
A is
boundary
and A3:
A is
Jordan
;
ex A1, A2 being Subset of (TOP-REAL 2) st
( A ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A = (Cl A1) \ A1 & ( for C1, C2 being Subset of ((TOP-REAL 2) | (A `)) st C1 = A1 & C2 = A2 holds
( C1 is a_component & C2 is a_component ) ) )consider A1,
A2 being
Subset of
(TOP-REAL 2) such that A4:
A ` = A1 \/ A2
and A5:
A1 misses A2
and A6:
(Cl A1) \ A1 = (Cl A2) \ A2
and A7:
for
C1,
C2 being
Subset of
((TOP-REAL 2) | (A `)) st
C1 = A1 &
C2 = A2 holds
(
C1 is
a_component &
C2 is
a_component )
by A3, JORDAN1:def 2;
A = (A1 \/ A2) `
by A4;
then A8:
A = (A1 `) /\ (A2 `)
by XBOOLE_1:53;
A2 c= A `
by A4, XBOOLE_1:7;
then reconsider D2 =
A2 as
Subset of
((TOP-REAL 2) | (A `)) by PRE_TOPC:8;
A1 c= A `
by A4, XBOOLE_1:7;
then reconsider D1 =
A1 as
Subset of
((TOP-REAL 2) | (A `)) by PRE_TOPC:8;
D2 = A2
;
then A9:
D1 is
a_component
by A7;
A10:
A c= (Cl A1) \ A1
(
(Cl A1) \ A1 c= A1 ` &
(Cl A2) \ A2 c= A2 ` )
by XBOOLE_1:33;
then
(Cl A1) \ A1 c= A
by A6, A8, XBOOLE_1:19;
then
A = (Cl A1) \ A1
by A10;
hence
ex
A1,
A2 being
Subset of
(TOP-REAL 2) st
(
A ` = A1 \/ A2 &
A1 misses A2 &
(Cl A1) \ A1 = (Cl A2) \ A2 &
A = (Cl A1) \ A1 & ( for
C1,
C2 being
Subset of
((TOP-REAL 2) | (A `)) st
C1 = A1 &
C2 = A2 holds
(
C1 is
a_component &
C2 is
a_component ) ) )
by A4, A5, A6, A7;
verum
end;