let T be non empty TopSpace; ( T is T_1 implies ex A, B being Subset of T st
( A \/ B = [#] T & A misses B & A is perfect & B is scattered ) )
defpred S1[ Subset of T] means $1 is dense-in-itself ;
consider CC being Subset-Family of T such that
A1:
for A being Subset of T holds
( A in CC iff S1[A] )
from SUBSET_1:sch 3();
set C = union CC;
A2:
( [#] T = (union CC) \/ ((union CC) `) & union CC misses (union CC) ` )
by PRE_TOPC:2, XBOOLE_1:79;
A3:
CC is dense-in-itself
by A1, Def9;
assume
T is T_1
; ex A, B being Subset of T st
( A \/ B = [#] T & A misses B & A is perfect & B is scattered )
then
Cl (union CC) is dense-in-itself
by A3, Th38, Th40;
then
Cl (union CC) in CC
by A1;
then A4:
Cl (union CC) c= union CC
by ZFMISC_1:74;
union CC c= Cl (union CC)
by PRE_TOPC:18;
then A5:
Cl (union CC) = union CC
by A4, XBOOLE_0:def 10;
for B being Subset of T holds
( B is empty or not B c= (union CC) ` or not B is dense-in-itself )
then A8:
(union CC) ` is scattered
by Def11;
union CC is dense-in-itself
by A3, Th40;
hence
ex A, B being Subset of T st
( A \/ B = [#] T & A misses B & A is perfect & B is scattered )
by A5, A8, A2; verum