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 :: thesis: for F being Subset-Family of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) st F c= the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) holds
union F in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #)
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 :: thesis: ( ( union F = D & union F in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) ) or ( union F <> D & union F in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) ) )
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 :: thesis: for A being Subset of D st A in F holds
not A = D
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:74;
hence contradiction by A4, XBOOLE_0:def 10; :: thesis: verum
end;
now :: thesis: for A being set st A in F holds
not d0 in A
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 :: thesis: for C, E being Subset of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) st 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 ) } ) #) holds
C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #)
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 :: thesis: for P being Subset of D st P in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) & P <> D holds
not d0 in P
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 :: thesis: ( ( C = D & E = D & C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) ) or ( ( C <> D or E <> D ) & C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) ) )
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 :: thesis: ( ( C <> D & C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) ) or ( E <> D & C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) ) )
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; :: thesis: verum