let X be non empty TopSpace; :: thesis:
let X0 be non empty SubSpace of X; :: thesis:
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;

hereby :: thesis:

assume X0 is maximal_discrete ; :: thesis:
then A1: A is maximal_discrete ;
then A is discrete ;
hence X0 is discrete by Th20; :: thesis:
thus for Y0 being non empty discrete SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) :: thesis:

let Y0 be non empty discrete SubSpace of X; :: thesis:
reconsider D = the carrier of Y0 as Subset of X by TSEP_1:1;
assume X0 is SubSpace of Y0 ; :: thesis:
then A2: A c= D by TSEP_1:4;
D is discrete by Th20;
then A = D by A1, A2;
hence TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) by TSEP_1:5; :: thesis:

end;

end;

hereby :: thesis:

assume X0 is discrete ; :: thesis:
then A3: A is discrete by Th20;
assume A4: for Y0 being non empty discrete SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ; :: thesis:

let D be Subset of X; :: thesis:
assume A5: D is discrete ; :: thesis:
assume A6: A c= D ; :: thesis:
then D <> {} ;
then consider Y0 being non empty strict discrete SubSpace of X such that
A7: D = the carrier of Y0 by A5, Th28;
X0 is SubSpace of Y0 by A6, A7, TSEP_1:4;
hence A = D by A4, A7; :: thesis:

end;

then A is maximal_discrete by A3;
hence X0 is maximal_discrete ; :: thesis:

end;