let Y be non empty TopStruct ; :: thesis: for Y0 being SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is maximal_discrete iff Y0 is maximal_discrete )
let Y0 be SubSpace of Y; :: thesis: for A being Subset of Y st A = the carrier of Y0 holds
( A is maximal_discrete iff Y0 is maximal_discrete )
let A be Subset of Y; :: thesis: ( A = the carrier of Y0 implies ( A is maximal_discrete iff Y0 is maximal_discrete ) )
assume A1: A = the carrier of Y0 ; :: thesis: ( A is maximal_discrete iff Y0 is maximal_discrete )

hereby :: thesis: ( Y0 is maximal_discrete implies A is maximal_discrete )

assume A is maximal_discrete ; :: thesis: Y0 is maximal_discrete
then for A being Subset of Y st A = the carrier of Y0 holds
A is maximal_discrete by A1;
hence Y0 is maximal_discrete by Def8; :: thesis: verum

end;

thus ( Y0 is maximal_discrete implies A is maximal_discrete ) by A1, Def8; :: thesis: verum