let X be non empty TopSpace; for A1, A2 being Subset of X
for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds
( A1,A2 are_separated iff B1,B2 are_separated )
let A1, A2 be Subset of X; for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds
( A1,A2 are_separated iff B1,B2 are_separated )
let X0 be non empty SubSpace of X; for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds
( A1,A2 are_separated iff B1,B2 are_separated )
let B1, B2 be Subset of X0; ( B1 = A1 & B2 = A2 implies ( A1,A2 are_separated iff B1,B2 are_separated ) )
assume that
A1:
B1 = A1
and
A2:
B2 = A2
; ( A1,A2 are_separated iff B1,B2 are_separated )
A3:
Cl B2 = (Cl A2) /\ ([#] X0)
by A2, PRE_TOPC:17;
A4:
Cl B1 = (Cl A1) /\ ([#] X0)
by A1, PRE_TOPC:17;
thus
( A1,A2 are_separated implies B1,B2 are_separated )
( B1,B2 are_separated implies A1,A2 are_separated )
thus
( B1,B2 are_separated implies A1,A2 are_separated )
verumproof
assume A7:
B1,
B2 are_separated
;
A1,A2 are_separated
then
(Cl A1) /\ ([#] X0) misses A2
by A2, A4, CONNSP_1:def 1;
then
((Cl A1) /\ ([#] X0)) /\ A2 = {}
;
then A8:
((Cl A1) /\ A2) /\ ([#] X0) = {}
by XBOOLE_1:16;
A1 misses (Cl A2) /\ ([#] X0)
by A1, A3, A7, CONNSP_1:def 1;
then
A1 /\ ((Cl A2) /\ ([#] X0)) = {}
;
then A9:
(A1 /\ (Cl A2)) /\ ([#] X0) = {}
by XBOOLE_1:16;
A1 /\ (Cl A2) c= A1
by XBOOLE_1:17;
then
A1 /\ (Cl A2) = {}
by A1, A9, XBOOLE_1:1, XBOOLE_1:28;
then A10:
A1 misses Cl A2
;
(Cl A1) /\ A2 c= A2
by XBOOLE_1:17;
then
(Cl A1) /\ A2 = {}
by A2, A8, XBOOLE_1:1, XBOOLE_1:28;
then
Cl A1 misses A2
;
hence
A1,
A2 are_separated
by A10, CONNSP_1:def 1;
verum
end;