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
reconsider E = D as Subset of D by Lm1;
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 ) } ;
then A2: 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 XBOOLE_0:def 5;

A3: 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 c= bool D & F misses { A where A is Subset of D : ( d0 in A & A <> D ) } ) by XBOOLE_1:63, XBOOLE_1:79;
then A4: ( F c= bool D & 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 A5: 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 ) } ) #)

A6: now

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

end;

now

let A be set ; :: thesis: ( A in F implies not d0 in A )
assume A8: 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 A4, A8, XBOOLE_0:def 4;
then ( not d0 in B or not B <> D ) ;
hence not d0 in A by A6, A8; :: 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;

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 A9: ( 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 ) } ) #) ) ; :: thesis: C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #)

A10: 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 A11: ( P in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) & P <> D ) ; :: thesis: not d0 in P
then not P in { A where A is Subset of D : ( d0 in A & A <> D ) } by XBOOLE_0:def 5;
hence not d0 in P by A11; :: 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 A12: ( 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 A12;

case 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 ) } ) #)

then ( not d0 in C & C /\ E c= C ) by A9, A10, XBOOLE_1:17;
then for A being Subset of D holds
( not A = C /\ E or not d0 in A or not A <> D ) ;
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 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 ) } ) #)

then ( not d0 in E & C /\ E c= E ) by A9, A10, XBOOLE_1:17;
then for A being Subset of D holds
( not A = C /\ E or not d0 in A or not A <> D ) ;
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;

hence STS D,d0 is TopSpace-like by A2, A3, PRE_TOPC:def 1; :: thesis: verum