let Y be TopStruct ; :: thesis: ( Y is discrete implies Y is TopSpace-like )
assume Y is discrete ; :: thesis: Y is TopSpace-like
then A1: the topology of Y = bool the carrier of Y ;
then A2: for F being Subset-Family of Y st F c= the topology of Y holds
union F in the topology of Y ;
A3: 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 A1;
the carrier of Y in the topology of Y by A1, ZFMISC_1:def 1;
hence Y is TopSpace-like by A2, A3, PRE_TOPC:def 1; :: thesis: verum