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 ) )
then A2: X1,X2 are_weakly_separated by TSEP_1:85;
thus X1 misses X2 by A1, TSEP_1:68; :: 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
thus 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 A2, Th126; :: 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

assume A3: 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 )
assume A4: 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
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
assume X1,X2 are_not_separated ; :: thesis: contradiction
then A5: 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 8;
A6: 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 A6, XBOOLE_1:7;
A7: ( Cl C1 = (Cl A1) /\ ([#] (X1 union X2)) & Cl C2 = (Cl A2) /\ ([#] (X1 union X2)) ) by PRE_TOPC:47;

A8: now

assume C1,C2 are_separated ; :: thesis: contradiction
then ( (Cl A1) /\ ([#] (X1 union X2)) misses A2 & A1 misses (Cl A2) /\ ([#] (X1 union X2)) ) by A7, CONNSP_1:def 1;
then ( ((Cl A1) /\ ([#] (X1 union X2))) /\ A2 = {} & A1 /\ ((Cl A2) /\ ([#] (X1 union X2))) = {} ) by XBOOLE_0:def 7;
then A9: ( ((Cl A1) /\ A2) /\ ([#] (X1 union X2)) = {} & (A1 /\ (Cl A2)) /\ ([#] (X1 union X2)) = {} ) by XBOOLE_1:16;
( C2 c= [#] (X1 union X2) & C1 c= [#] (X1 union X2) ) ;
then ( (Cl A1) /\ A2 c= A2 & A1 /\ (Cl A2) c= A1 & A2 c= [#] (X1 union X2) & A1 c= [#] (X1 union X2) ) by XBOOLE_1:17;
then ( (Cl A1) /\ A2 = {} & A1 /\ (Cl A2) = {} ) by A9, XBOOLE_1:1, XBOOLE_1:28;
then ( Cl A1 misses A2 & A1 misses Cl A2 ) by XBOOLE_0:def 7;
hence contradiction by A5, CONNSP_1:def 1; :: thesis: verum

end;

A10: C1 misses C2 by A3, TSEP_1:def 3;
reconsider Y1 = X1, Y2 = X2 as SubSpace of X1 union X2 by TSEP_1:22;

now

per cases ( not C1 is open or not C2 is open ) by A8, A10, TSEP_1:41;

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

set Y = (X1 union X2) modified_with_respect_to C1;
set g = modid (X1 union X2),C1;
A12: modid (X1 union X2),C1 is not continuous Function of (X1 union X2),((X1 union X2) modified_with_respect_to C1) by A11, Th113;
A13: (modid (X1 union X2),C1) | Y1 = (modid (X1 union X2),C1) | X1 by Def4;
(modid (X1 union X2),C1) | Y2 = (modid (X1 union X2),C1) | X2 by Def4;
then ( (modid (X1 union X2),C1) | X1 is continuous Function of X1,((X1 union X2) modified_with_respect_to C1) & (modid (X1 union X2),C1) | X2 is continuous Function of X2,((X1 union X2) modified_with_respect_to C1) ) by A10, A13, Th111, Th112;
hence contradiction by A4, A12; :: thesis: verum

end;

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

set Y = (X1 union X2) modified_with_respect_to C2;
set g = modid (X1 union X2),C2;
A15: modid (X1 union X2),C2 is not continuous Function of (X1 union X2),((X1 union X2) modified_with_respect_to C2) by A14, Th113;
A16: (modid (X1 union X2),C2) | Y1 = (modid (X1 union X2),C2) | X1 by Def4;
(modid (X1 union X2),C2) | Y2 = (modid (X1 union X2),C2) | X2 by Def4;
then ( (modid (X1 union X2),C2) | X1 is continuous Function of X1,((X1 union X2) modified_with_respect_to C2) & (modid (X1 union X2),C2) | X2 is continuous Function of X2,((X1 union X2) modified_with_respect_to C2) ) by A10, A16, Th111, Th112;
hence contradiction by A4, A15; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;