for X being non empty TopSpace
for M being Subset of X st M is maximal_T_0 holds
for A being Subset of X holds Int A = MaxADSet (M /\ (Int A)) by Th6;