thus 1TopSp D is strict ; :: thesis: 1TopSp D is TopSpace-like
set T = 1TopSp D;
A1: for X being Subset-Family of (1TopSp D) st X c= the topology of (1TopSp D) holds
union X in the topology of (1TopSp D) ;
A2: for p, q being Subset of (1TopSp D) st p in the topology of (1TopSp D) & q in the topology of (1TopSp D) holds
p /\ q in the topology of (1TopSp D) ;
D in bool D by ZFMISC_1:def 1;
hence 1TopSp D is TopSpace-like by A1, A2, PRE_TOPC:def 1; :: thesis: verum