let T be non empty TopSpace; :: thesis: ( 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;
assume T is T_1 ; :: thesis: 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, Th36, Th38;
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;
for B being Subset of T holds
( B is empty or not B c= (union CC) ` or not B is dense-in-itself )
proof
given B being Subset of T such that A6: not B is empty and
A7: ( B c= (union CC) ` & B is dense-in-itself ) ; :: thesis: contradiction
( B misses union CC & B in CC ) by A1, A7, SUBSET_1:23;
hence contradiction by A6, XBOOLE_1:69, ZFMISC_1:74; :: thesis: verum
end;
then A8: (union CC) ` is scattered ;
union CC is dense-in-itself by A3, Th38;
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; :: thesis: verum