consider a being object such that

A1: a in the carrier of X by XBOOLE_0:def 1;

reconsider a = a as Point of X by A1;

consider X0 being non empty strict SubSpace of X such that

A2: MaxADSet a = the carrier of X0 by TSEP_1:10;

take X0 ; :: thesis: ( X0 is maximal_anti-discrete & X0 is strict )

MaxADSet a is maximal_anti-discrete by Th20;

hence ( X0 is maximal_anti-discrete & X0 is strict ) by A2, Th72; :: thesis: verum

A1: a in the carrier of X by XBOOLE_0:def 1;

reconsider a = a as Point of X by A1;

consider X0 being non empty strict SubSpace of X such that

A2: MaxADSet a = the carrier of X0 by TSEP_1:10;

take X0 ; :: thesis: ( X0 is maximal_anti-discrete & X0 is strict )

MaxADSet a is maximal_anti-discrete by Th20;

hence ( X0 is maximal_anti-discrete & X0 is strict ) by A2, Th72; :: thesis: verum