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 )
proof
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 ;
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;
thus ( 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 ) :: 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 ;
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 ;
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 ;
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 ;
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 ;
then Cl A1 misses A2 ;
hence contradiction by A7, A12, CONNSP_1:def 1; :: thesis: verum
end;
per cases ( not C1 is open or not C2 is open ) by ;
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 ;
modid ((X1 union X2),C1) is not continuous Function of (X1 union X2),((X1 union X2) modified_with_respect_to C1) by ;
hence contradiction by A6, A14, A15; :: thesis: verum
end;
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 ;
modid ((X1 union X2),C2) is not continuous Function of (X1 union X2),((X1 union X2) modified_with_respect_to C2) by ;
hence contradiction by A6, A18, A17; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;