let X0 be non empty SubSpace of X; :: thesis: ( X0 is open & X0 is anti-discrete implies X0 is maximal_anti-discrete )

reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;

assume X0 is open ; :: thesis: ( not X0 is anti-discrete or X0 is maximal_anti-discrete )

then A1: A is open by TSEP_1:16;

assume X0 is anti-discrete ; :: thesis: X0 is maximal_anti-discrete

then A is anti-discrete by Th66;

then A is maximal_anti-discrete by A1, Th16;

hence X0 is maximal_anti-discrete by Th72; :: thesis: verum

reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;

assume X0 is open ; :: thesis: ( not X0 is anti-discrete or X0 is maximal_anti-discrete )

then A1: A is open by TSEP_1:16;

assume X0 is anti-discrete ; :: thesis: X0 is maximal_anti-discrete

then A is anti-discrete by Th66;

then A is maximal_anti-discrete by A1, Th16;

hence X0 is maximal_anti-discrete by Th72; :: thesis: verum