let X be non empty TopSpace; for X1, X2 being non empty SubSpace of X holds
( X1,X2 are_separated iff ex Y1, Y2 being non empty open SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 ) )
let X1, X2 be non empty SubSpace of X; ( X1,X2 are_separated iff ex Y1, Y2 being non empty open SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 ) )
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
thus
( X1,X2 are_separated implies ex Y1, Y2 being non empty open SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 ) )
( ex Y1, Y2 being non empty open SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 ) implies X1,X2 are_separated )proof
assume
X1,
X2 are_separated
;
ex Y1, Y2 being non empty open SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 )
then
A1,
A2 are_separated
;
then consider C1,
C2 being
Subset of
X such that A1:
A1 c= C1
and A2:
A2 c= C2
and A3:
(
C1 misses A2 &
C2 misses A1 )
and A4:
C1 is
open
and A5:
C2 is
open
by Th44;
not
C1 is
empty
by A1, XBOOLE_1:3;
then consider Y1 being non
empty strict open SubSpace of
X such that A6:
C1 = the
carrier of
Y1
by A4, Th20;
not
C2 is
empty
by A2, XBOOLE_1:3;
then consider Y2 being non
empty strict open SubSpace of
X such that A7:
C2 = the
carrier of
Y2
by A5, Th20;
take
Y1
;
ex Y2 being non empty open SubSpace of X st
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 )
take
Y2
;
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 )
thus
(
X1 is
SubSpace of
Y1 &
X2 is
SubSpace of
Y2 &
Y1 misses X2 &
Y2 misses X1 )
by A1, A2, A3, A6, A7, Th4;
verum
end;
given Y1, Y2 being non empty open SubSpace of X such that A8:
( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1 )
; X1,X2 are_separated
hence
X1,X2 are_separated
; verum