let Y be TopStruct ; :: thesis: ( Y is discrete implies Y is TopSpace-like )
assume Y is discrete ; :: thesis: Y is TopSpace-like
then the topology of Y = bool the carrier of Y by Def1;
then ( the carrier of Y in the topology of Y & ( for F being Subset-Family of Y st F c= the topology of Y holds
union F in the topology of Y ) & ( for A, B being Subset of Y st A in the topology of Y & B in the topology of Y holds
A /\ B in the topology of Y ) ) by ZFMISC_1:def 1;
hence Y is TopSpace-like by PRE_TOPC:def 1; :: thesis: verum