reconsider E = D as Subset of D by Lm1;
set G = { A where A is Subset of D : ( d0 in A & A <> D ) } ;
set T = (bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ;
set Y = TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #);
thus STS D,d0 is strict ; :: thesis: STS D,d0 is TopSpace-like
for A being Subset of D holds
( not A = E or not d0 in A or not A <> D ) ;
then A1: not E in { A where A is Subset of D : ( d0 in A & A <> D ) } ;

A2: now

let F be Subset-Family of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #); :: thesis: ( F c= the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) implies union F in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) )
assume F c= the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) ; :: thesis: union F in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #)
then F misses { A where A is Subset of D : ( d0 in A & A <> D ) } by XBOOLE_1:63, XBOOLE_1:79;
then A3: F /\ { A where A is Subset of D : ( d0 in A & A <> D ) } = {} by XBOOLE_0:def 7;

now

per cases ( union F = D or union F <> D ) ;

case union F = D ; :: thesis: union F in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #)

hence union F in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) by A1, XBOOLE_0:def 5; :: thesis: verum

end;

case A4: union F <> D ; :: thesis: union F in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #)

A5: now

let A be Subset of D; :: thesis: ( A in F implies not A = D )
assume A6: A in F ; :: thesis: not A = D
assume A = D ; :: thesis: contradiction
then D c= union F by A6, ZFMISC_1:92;
hence contradiction by A4, XBOOLE_0:def 10; :: thesis: verum

end;

now

let A be set ; :: thesis: ( A in F implies not d0 in A )
assume A7: A in F ; :: thesis: not d0 in A
then reconsider B = A as Subset of D ;
not B in { A where A is Subset of D : ( d0 in A & A <> D ) } by A3, A7, XBOOLE_0:def 4;
then ( not d0 in B or not B <> D ) ;
hence not d0 in A by A5, A7; :: thesis: verum

end;

then for A being set holds
( not d0 in A or not A in F ) ;
then for A being Subset of D holds
( not A = union F or not d0 in A or not A <> D ) by TARSKI:def 4;
then not union F in { A where A is Subset of D : ( d0 in A & A <> D ) } ;
hence union F in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) by XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

hence union F in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) ; :: thesis: verum

end;

A8: now

let C, E be Subset of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #); :: thesis: ( C in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) & E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) implies C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) )
assume that
A9: C in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) and
A10: E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) ; :: thesis: C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #)

A11: now

let P be Subset of D; :: thesis: ( P in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) & P <> D implies not d0 in P )
assume that
A12: P in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) and
A13: P <> D ; :: thesis: not d0 in P
not P in { A where A is Subset of D : ( d0 in A & A <> D ) } by A12, XBOOLE_0:def 5;
hence not d0 in P by A13; :: thesis: verum

end;

now

per cases ( ( C = D & E = D ) or C <> D or E <> D ) ;

case ( C = D & E = D ) ; :: thesis: C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #)

hence C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) by A1, XBOOLE_0:def 5; :: thesis: verum

end;

case A14: ( C <> D or E <> D ) ; :: thesis: C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #)

now

per cases ( C <> D or E <> D ) by A14;

case A15: C <> D ; :: thesis: C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #)

C /\ E c= C by XBOOLE_1:17;
then for A being Subset of D holds
( not A = C /\ E or not d0 in A or not A <> D ) by A9, A11, A15;
then not C /\ E in { A where A is Subset of D : ( d0 in A & A <> D ) } ;
hence C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) by XBOOLE_0:def 5; :: thesis: verum

end;

case A16: E <> D ; :: thesis: C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #)

C /\ E c= E by XBOOLE_1:17;
then for A being Subset of D holds
( not A = C /\ E or not d0 in A or not A <> D ) by A10, A11, A16;
then not C /\ E in { A where A is Subset of D : ( d0 in A & A <> D ) } ;
hence C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) by XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

hence C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) ; :: thesis: verum

end;

end;

end;

hence C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) ; :: thesis: verum

end;

the carrier of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) by A1, XBOOLE_0:def 5;
hence STS D,d0 is TopSpace-like by A2, A8, PRE_TOPC:def 1; :: thesis: verum