let X be non empty TopSpace; :: thesis: for X1, X2 being non empty SubSpace of X holds

( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace

for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

g is continuous Function of (X1 union X2),Y ) ) )

let X1, X2 be non empty SubSpace of X; :: thesis: ( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace

for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

g is continuous Function of (X1 union X2),Y ) ) )

thus ( X1,X2 are_separated implies ( X1 misses X2 & ( for Y being non empty TopSpace

for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

g is continuous Function of (X1 union X2),Y ) ) ) :: thesis: ( X1 misses X2 & ( for Y being non empty TopSpace

for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

g is continuous Function of (X1 union X2),Y ) implies X1,X2 are_separated )

for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

g is continuous Function of (X1 union X2),Y ) implies X1,X2 are_separated ) :: thesis: verum

( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace

for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

g is continuous Function of (X1 union X2),Y ) ) )

let X1, X2 be non empty SubSpace of X; :: thesis: ( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace

for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

g is continuous Function of (X1 union X2),Y ) ) )

thus ( X1,X2 are_separated implies ( X1 misses X2 & ( for Y being non empty TopSpace

for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

g is continuous Function of (X1 union X2),Y ) ) ) :: thesis: ( X1 misses X2 & ( for Y being non empty TopSpace

for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

g is continuous Function of (X1 union X2),Y ) implies X1,X2 are_separated )

proof

thus
( X1 misses X2 & ( for Y being non empty TopSpace
assume A1:
X1,X2 are_separated
; :: thesis: ( X1 misses X2 & ( for Y being non empty TopSpace

for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

g is continuous Function of (X1 union X2),Y ) )

hence X1 misses X2 by TSEP_1:63; :: thesis: for Y being non empty TopSpace

for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

g is continuous Function of (X1 union X2),Y

X1,X2 are_weakly_separated by A1, TSEP_1:78;

hence for Y being non empty TopSpace

for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

g is continuous Function of (X1 union X2),Y by Th114; :: thesis: verum

end;for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

g is continuous Function of (X1 union X2),Y ) )

hence X1 misses X2 by TSEP_1:63; :: thesis: for Y being non empty TopSpace

for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

g is continuous Function of (X1 union X2),Y

X1,X2 are_weakly_separated by A1, TSEP_1:78;

hence for Y being non empty TopSpace

for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

g is continuous Function of (X1 union X2),Y by Th114; :: thesis: verum

for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

g is continuous Function of (X1 union X2),Y ) implies X1,X2 are_separated ) :: thesis: verum

proof

reconsider Y1 = X1, Y2 = X2 as SubSpace of X1 union X2 by TSEP_1:22;

reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;

reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;

A2: the carrier of (X1 union X2) = A1 \/ A2 by TSEP_1:def 2;

then reconsider C1 = A1 as Subset of (X1 union X2) by XBOOLE_1:7;

reconsider C2 = A2 as Subset of (X1 union X2) by A2, XBOOLE_1:7;

A3: Cl C1 = (Cl A1) /\ ([#] (X1 union X2)) by PRE_TOPC:17;

A4: Cl C2 = (Cl A2) /\ ([#] (X1 union X2)) by PRE_TOPC:17;

assume X1 misses X2 ; :: thesis: ( ex Y being non empty TopSpace ex g being Function of (X1 union X2),Y st

( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y & g is not continuous Function of (X1 union X2),Y ) or X1,X2 are_separated )

then A5: C1 misses C2 by TSEP_1:def 3;

assume A6: for Y being non empty TopSpace

for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

g is continuous Function of (X1 union X2),Y ; :: thesis: X1,X2 are_separated

assume X1,X2 are_not_separated ; :: thesis: contradiction

then A7: ex A10, A20 being Subset of X st

( A10 = the carrier of X1 & A20 = the carrier of X2 & A10,A20 are_not_separated ) by TSEP_1:def 6;

end;reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;

reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;

A2: the carrier of (X1 union X2) = A1 \/ A2 by TSEP_1:def 2;

then reconsider C1 = A1 as Subset of (X1 union X2) by XBOOLE_1:7;

reconsider C2 = A2 as Subset of (X1 union X2) by A2, XBOOLE_1:7;

A3: Cl C1 = (Cl A1) /\ ([#] (X1 union X2)) by PRE_TOPC:17;

A4: Cl C2 = (Cl A2) /\ ([#] (X1 union X2)) by PRE_TOPC:17;

assume X1 misses X2 ; :: thesis: ( ex Y being non empty TopSpace ex g being Function of (X1 union X2),Y st

( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y & g is not continuous Function of (X1 union X2),Y ) or X1,X2 are_separated )

then A5: C1 misses C2 by TSEP_1:def 3;

assume A6: for Y being non empty TopSpace

for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

g is continuous Function of (X1 union X2),Y ; :: thesis: X1,X2 are_separated

assume X1,X2 are_not_separated ; :: thesis: contradiction

then A7: ex A10, A20 being Subset of X st

( A10 = the carrier of X1 & A20 = the carrier of X2 & A10,A20 are_not_separated ) by TSEP_1:def 6;

A8: now :: thesis: not C1,C2 are_separated

assume A9:
C1,C2 are_separated
; :: thesis: contradiction

then (Cl A1) /\ ([#] (X1 union X2)) misses A2 by A3, CONNSP_1:def 1;

then ((Cl A1) /\ ([#] (X1 union X2))) /\ A2 = {} ;

then A10: ((Cl A1) /\ A2) /\ ([#] (X1 union X2)) = {} by XBOOLE_1:16;

A1 misses (Cl A2) /\ ([#] (X1 union X2)) by A4, A9, CONNSP_1:def 1;

then A1 /\ ((Cl A2) /\ ([#] (X1 union X2))) = {} ;

then A11: (A1 /\ (Cl A2)) /\ ([#] (X1 union X2)) = {} by XBOOLE_1:16;

( C1 c= [#] (X1 union X2) & A1 /\ (Cl A2) c= A1 ) by XBOOLE_1:17;

then A1 /\ (Cl A2) = {} by A11, XBOOLE_1:1, XBOOLE_1:28;

then A12: A1 misses Cl A2 ;

( C2 c= [#] (X1 union X2) & (Cl A1) /\ A2 c= A2 ) by XBOOLE_1:17;

then (Cl A1) /\ A2 = {} by A10, XBOOLE_1:1, XBOOLE_1:28;

then Cl A1 misses A2 ;

hence contradiction by A7, A12, CONNSP_1:def 1; :: thesis: verum

end;then (Cl A1) /\ ([#] (X1 union X2)) misses A2 by A3, CONNSP_1:def 1;

then ((Cl A1) /\ ([#] (X1 union X2))) /\ A2 = {} ;

then A10: ((Cl A1) /\ A2) /\ ([#] (X1 union X2)) = {} by XBOOLE_1:16;

A1 misses (Cl A2) /\ ([#] (X1 union X2)) by A4, A9, CONNSP_1:def 1;

then A1 /\ ((Cl A2) /\ ([#] (X1 union X2))) = {} ;

then A11: (A1 /\ (Cl A2)) /\ ([#] (X1 union X2)) = {} by XBOOLE_1:16;

( C1 c= [#] (X1 union X2) & A1 /\ (Cl A2) c= A1 ) by XBOOLE_1:17;

then A1 /\ (Cl A2) = {} by A11, XBOOLE_1:1, XBOOLE_1:28;

then A12: A1 misses Cl A2 ;

( C2 c= [#] (X1 union X2) & (Cl A1) /\ A2 c= A2 ) by XBOOLE_1:17;

then (Cl A1) /\ A2 = {} by A10, XBOOLE_1:1, XBOOLE_1:28;

then Cl A1 misses A2 ;

hence contradiction by A7, A12, CONNSP_1:def 1; :: thesis: verum

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( not C1 is open or not C2 is open )
by A8, A5, TSEP_1:37;

end;

suppose A13:
not C1 is open
; :: thesis: contradiction

set g = modid ((X1 union X2),C1);

set Y = (X1 union X2) modified_with_respect_to C1;

(modid ((X1 union X2),C1)) | Y1 = (modid ((X1 union X2),C1)) | X1 by Def5;

then A14: (modid ((X1 union X2),C1)) | X1 is continuous Function of X1,((X1 union X2) modified_with_respect_to C1) by Th100;

(modid ((X1 union X2),C1)) | Y2 = (modid ((X1 union X2),C1)) | X2 by Def5;

then A15: (modid ((X1 union X2),C1)) | X2 is continuous Function of X2,((X1 union X2) modified_with_respect_to C1) by A5, Th99;

modid ((X1 union X2),C1) is not continuous Function of (X1 union X2),((X1 union X2) modified_with_respect_to C1) by A13, Th101;

hence contradiction by A6, A14, A15; :: thesis: verum

end;set Y = (X1 union X2) modified_with_respect_to C1;

(modid ((X1 union X2),C1)) | Y1 = (modid ((X1 union X2),C1)) | X1 by Def5;

then A14: (modid ((X1 union X2),C1)) | X1 is continuous Function of X1,((X1 union X2) modified_with_respect_to C1) by Th100;

(modid ((X1 union X2),C1)) | Y2 = (modid ((X1 union X2),C1)) | X2 by Def5;

then A15: (modid ((X1 union X2),C1)) | X2 is continuous Function of X2,((X1 union X2) modified_with_respect_to C1) by A5, Th99;

modid ((X1 union X2),C1) is not continuous Function of (X1 union X2),((X1 union X2) modified_with_respect_to C1) by A13, Th101;

hence contradiction by A6, A14, A15; :: thesis: verum

suppose A16:
not C2 is open
; :: thesis: contradiction

set g = modid ((X1 union X2),C2);

set Y = (X1 union X2) modified_with_respect_to C2;

(modid ((X1 union X2),C2)) | Y2 = (modid ((X1 union X2),C2)) | X2 by Def5;

then A17: (modid ((X1 union X2),C2)) | X2 is continuous Function of X2,((X1 union X2) modified_with_respect_to C2) by Th100;

(modid ((X1 union X2),C2)) | Y1 = (modid ((X1 union X2),C2)) | X1 by Def5;

then A18: (modid ((X1 union X2),C2)) | X1 is continuous Function of X1,((X1 union X2) modified_with_respect_to C2) by A5, Th99;

modid ((X1 union X2),C2) is not continuous Function of (X1 union X2),((X1 union X2) modified_with_respect_to C2) by A16, Th101;

hence contradiction by A6, A18, A17; :: thesis: verum

end;set Y = (X1 union X2) modified_with_respect_to C2;

(modid ((X1 union X2),C2)) | Y2 = (modid ((X1 union X2),C2)) | X2 by Def5;

then A17: (modid ((X1 union X2),C2)) | X2 is continuous Function of X2,((X1 union X2) modified_with_respect_to C2) by Th100;

(modid ((X1 union X2),C2)) | Y1 = (modid ((X1 union X2),C2)) | X1 by Def5;

then A18: (modid ((X1 union X2),C2)) | X1 is continuous Function of X1,((X1 union X2) modified_with_respect_to C2) by A5, Th99;

modid ((X1 union X2),C2) is not continuous Function of (X1 union X2),((X1 union X2) modified_with_respect_to C2) by A16, Th101;

hence contradiction by A6, A18, A17; :: thesis: verum