set C = bool {{},1};
set Y = ADTS (bool {{},1});
A1: 1 in {{},1} by TARSKI:def 2;
{} in {{},1} by TARSKI:def 2;
then reconsider B0 = {{}}, B1 = {1} as Subset of {{},1} by A1, ZFMISC_1:31;
A2: {} c= {{},1} by XBOOLE_1:2;
then reconsider A = {{}} as Subset of (ADTS (bool {{},1})) by ZFMISC_1:31;
set Y1 = (ADTS (bool {{},1})) modified_with_respect_to A;
A3: the carrier of ((ADTS (bool {{},1})) modified_with_respect_to A) = the carrier of (ADTS (bool {{},1})) by TMAP_1:93;
reconsider A1 = A as Subset of ((ADTS (bool {{},1})) modified_with_respect_to A) by TMAP_1:93;
set Y2 = ((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `);
reconsider A2 = A1 as Subset of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) by TMAP_1:93;
set A3 = A2 ` ;
A4: the carrier of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) = the carrier of ((ADTS (bool {{},1})) modified_with_respect_to A) by TMAP_1:93;
then reconsider B = {B0,B1} as non empty Subset of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) by TMAP_1:93;

now :: thesis:

let H be object ; :: thesis:
assume H in the topology of ((ADTS (bool {{},1})) modified_with_respect_to A) ; :: thesis:
then H in A -extension_of_the_topology_of (ADTS (bool {{},1})) by TMAP_1:93;
then H in { (p \/ (q /\ A)) where p, q is Subset of (ADTS (bool {{},1})) : ( p in the topology of (ADTS (bool {{},1})) & q in the topology of (ADTS (bool {{},1})) ) } by TMAP_1:def 7;
then consider P, Q being Subset of (ADTS (bool {{},1})) such that
A5: H = P \/ (Q /\ A) and
A6: P in the topology of (ADTS (bool {{},1})) and
A7: Q in the topology of (ADTS (bool {{},1})) ;

now :: thesis:

per cases by A6, A7, TARSKI:def 2;

case ( P = {} & Q = {} ) ; :: thesis:

hence H = {} by A5; :: thesis:

end;

case ( P = bool {{},1} & Q = {} ) ; :: thesis:

hence H = bool {{},1} by A5; :: thesis:

end;

case ( P = {} & Q = bool {{},1} ) ; :: thesis:

hence H = A by A5, XBOOLE_1:28; :: thesis:

end;

case ( P = bool {{},1} & Q = bool {{},1} ) ; :: thesis:

hence H = bool {{},1} by A5, XBOOLE_1:12; :: thesis:

end;

end;

end;

hence H in {{},A1,(bool {{},1})} by ENUMSET1:def 1; :: thesis:

end;

then A8: the topology of ((ADTS (bool {{},1})) modified_with_respect_to A) c= {{},A1,(bool {{},1})} by TARSKI:def 3;

now :: thesis:

let H be object ; :: thesis:
assume H in the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) ; :: thesis:
then H in (A1 `) -extension_of_the_topology_of ((ADTS (bool {{},1})) modified_with_respect_to A) by TMAP_1:93;
then H in { (P \/ (Q /\ (A1 `))) where P, Q is Subset of ((ADTS (bool {{},1})) modified_with_respect_to A) : ( P in the topology of ((ADTS (bool {{},1})) modified_with_respect_to A) & Q in the topology of ((ADTS (bool {{},1})) modified_with_respect_to A) ) } by TMAP_1:def 7;
then consider P, Q being Subset of ((ADTS (bool {{},1})) modified_with_respect_to A) such that
A9: H = P \/ (Q /\ (A1 `)) and
A10: P in the topology of ((ADTS (bool {{},1})) modified_with_respect_to A) and
A11: Q in the topology of ((ADTS (bool {{},1})) modified_with_respect_to A) ;

now :: thesis:

per cases by A8, A10, A11, ENUMSET1:def 1;

case ( P = {} & Q = {} ) ; :: thesis:

hence H = {} by A9; :: thesis:

end;

case ( P = A1 & Q = {} ) ; :: thesis:

hence H = A1 by A9; :: thesis:

end;

case ( P = bool {{},1} & Q = {} ) ; :: thesis:

hence H = bool {{},1} by A9; :: thesis:

end;

case A12: ( P = {} & Q = A1 ) ; :: thesis:

A1 misses A1 ` by XBOOLE_1:79;
hence H = {} by A9, A12, XBOOLE_0:def 7; :: thesis:

end;

case A13: ( P = A1 & Q = A1 ) ; :: thesis:

A1 misses A1 ` by XBOOLE_1:79;
then A1 /\ (A1 `) = {} ((ADTS (bool {{},1})) modified_with_respect_to A) by XBOOLE_0:def 7;
hence H = A1 by A9, A13; :: thesis:

end;

case A14: ( P = bool {{},1} & Q = A1 ) ; :: thesis:

A1 misses A1 ` by XBOOLE_1:79;
then A1 /\ (A1 `) = {} ((ADTS (bool {{},1})) modified_with_respect_to A) by XBOOLE_0:def 7;
hence H = bool {{},1} by A9, A14; :: thesis:

end;

case ( P = {} & Q = bool {{},1} ) ; :: thesis:

hence H = A2 ` by A3, A4, A9, XBOOLE_1:28; :: thesis:

end;

case A15: ( P = A1 & Q = bool {{},1} ) ; :: thesis:

A1 \/ (A1 `) = [#] ((ADTS (bool {{},1})) modified_with_respect_to A) by PRE_TOPC:2;
hence H = bool {{},1} by A3, A9, A15, XBOOLE_1:28; :: thesis:

end;

case ( P = bool {{},1} & Q = bool {{},1} ) ; :: thesis:

hence H = bool {{},1} by A3, A9, XBOOLE_1:12; :: thesis:

end;

end;

end;

hence H in {{},A2,(A2 `),(bool {{},1})} by ENUMSET1:def 2; :: thesis:

end;

then A16: the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) c= {{},A2,(A2 `),(bool {{},1})} by TARSKI:def 3;
A17: A2 is open by Th1, TMAP_1:94;
A18: A2 is closed by Th3;

now :: thesis:

let H be object ; :: thesis:
assume H in {{},A2,(A2 `),(bool {{},1})} ; :: thesis:
then ( H = {} or H = A2 or H = A2 ` or H = bool {{},1} ) by ENUMSET1:def 2;
hence H in the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) by A3, A4, A18, A17, PRE_TOPC:1, PRE_TOPC:def 2; :: thesis:

end;

then {{},A2,(A2 `),(bool {{},1})} c= the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) by TARSKI:def 3;
then A19: the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) = {{},A2,(A2 `),(bool {{},1})} by A16, XBOOLE_0:def 10;

A20: now :: thesis:

let G be Subset of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)); :: thesis:
A21: ( ( G = {} or G = bool {{},1} ) implies G is closed ) by A4, TMAP_1:93;

A22: now :: thesis:

A2 ` in the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) by A19, ENUMSET1:def 2;
then A23: A2 ` is open ;
assume G = A2 ; :: thesis:
hence G is closed by A23; :: thesis:

end;

A24: now :: thesis:

A2 in the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) by A19, ENUMSET1:def 2;
then A25: (A2 `) ` is open ;
assume G = A2 ` ; :: thesis:
hence G is closed by A25; :: thesis:

end;

assume G is open ; :: thesis:
then G in {{},A2,(A2 `),(bool {{},1})} by A19;
hence G is closed by A21, A22, A24, ENUMSET1:def 2; :: thesis:

end;

A26: {} in bool {{},1} by A2;

A27: now :: thesis:

A28: now :: thesis:

reconsider I = {{},1} as Point of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) by A3, A4, ZFMISC_1:def 1;
A29: not I in A2 by TARSKI:def 1;
A30: Int B c= B by TOPS_1:16;
assume Int B = A2 ` ; :: thesis:
then I in Int B by A29, SUBSET_1:29;
then ( I = B0 or I = B1 ) by A30, TARSKI:def 2;
then ( 1 in B0 or {} in B1 ) by TARSKI:def 2;
hence contradiction by TARSKI:def 1; :: thesis:

end;

take B = B; :: thesis:

A31: now :: thesis:

assume Int B = A2 ; :: thesis:
then A32: {} in Int B by TARSKI:def 1;
Int B c= B by TOPS_1:16;
hence contradiction by A32, TARSKI:def 2; :: thesis:

end;

A33: now :: thesis:

assume Int B = bool {{},1} ; :: thesis:
then bool {{},1} c= B by TOPS_1:16;
hence contradiction by A26, TARSKI:def 2; :: thesis:

end;

Int B in {{},A2,(A2 `),(bool {{},1})} by A19, PRE_TOPC:def 2;
then ( Int B = {} or Int B = A2 or Int B = A2 ` or Int B = bool {{},1} ) by ENUMSET1:def 2;
hence B is boundary by A33, A31, A28, TOPS_1:48; :: thesis:

end;

take ((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `) ; :: thesis:

now :: thesis:

take A2 = A2; :: thesis:

now :: thesis:

assume A2 = bool {{},1} ; :: thesis:
then B0 = {} by TARSKI:def 1;
hence contradiction ; :: thesis:

end;

hence ( A2 is open & A2 <> {} & A2 <> the carrier of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) ) by A4, Th1, TMAP_1:93, TMAP_1:94; :: thesis:

end;

hence ( ((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `) is almost_discrete & not ((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `) is discrete & not ((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `) is anti-discrete & ((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `) is strict & not ((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `) is empty ) by A27, A20, TDLAT_3:18, TDLAT_3:21; :: thesis: