let Y be 1 -element TopStruct ; :: thesis: ( not the topology of Y is empty & Y is almost_discrete implies Y is TopSpace-like )
consider d being Element of Y such that
A1: the carrier of Y = {d} by Def1;
reconsider D = {d} as Subset of Y ;
assume not the topology of Y is empty ; :: thesis: ( not Y is almost_discrete or Y is TopSpace-like )
then consider A being Subset of Y such that
A2: A in the topology of Y by SUBSET_1:4;
assume A3: for A being Subset of Y st A in the topology of Y holds
the carrier of Y \ A in the topology of Y ; :: according to TDLAT_3:def 3 :: thesis: Y is TopSpace-like
A4: bool D = {{},D} by ZFMISC_1:24;
now :: thesis: {{},D} c= the topology of Y
per cases ( A = {} or A = D ) by A1, A4, TARSKI:def 2;
suppose A5: A = {} ; :: thesis: {{},D} c= the topology of Y
D \ A in the topology of Y by A1, A2, A3;
hence {{},D} c= the topology of Y by A2, A5, ZFMISC_1:32; :: thesis: verum
end;
suppose A6: A = D ; :: thesis: {{},D} c= the topology of Y
D \ A in the topology of Y by A1, A2, A3;
then {} in the topology of Y by A6, XBOOLE_1:37;
hence {{},D} c= the topology of Y by A2, A6, ZFMISC_1:32; :: thesis: verum
end;
end;
end;
then the topology of Y = {{}, the carrier of Y} by A1, A4, XBOOLE_0:def 10;
then reconsider Y = Y as anti-discrete TopStruct by TDLAT_3:def 2;
Y is TopSpace-like ;
hence Y is TopSpace-like ; :: thesis: verum