let X be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X holds
( X0 is maximal_discrete iff ( X0 is discrete & ( 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 #) ) ) )
let X0 be non empty SubSpace of X; :: thesis: ( X0 is maximal_discrete iff ( X0 is discrete & ( 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 #) ) ) )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;

hereby :: thesis: ( X0 is discrete & ( 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 #) ) implies X0 is maximal_discrete )

assume X0 is maximal_discrete ; :: thesis: ( X0 is discrete & ( 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 #) ) )
then A1: A is maximal_discrete ;
then A is discrete ;
hence X0 is discrete by Th20; :: thesis: 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 #)
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: verum

proof

let Y0 be non empty discrete SubSpace of X; :: thesis: ( X0 is SubSpace of Y0 implies TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) )
reconsider D = the carrier of Y0 as Subset of X by TSEP_1:1;
assume X0 is SubSpace of Y0 ; :: thesis: TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #)
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: verum

end;

end;

hereby :: thesis: verum

assume X0 is discrete ; :: thesis: ( ( 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 #) ) implies X0 is maximal_discrete )
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: X0 is maximal_discrete

now :: thesis: for D being Subset of X st D is discrete & A c= D holds
A = D

let D be Subset of X; :: thesis: ( D is discrete & A c= D implies A = D )
assume A5: D is discrete ; :: thesis: ( A c= D implies A = D )
assume A6: A c= D ; :: thesis: A = D
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: verum

end;

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

end;