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: for H being object st H in the topology of ((ADTS (bool {{},1})) modified_with_respect_to A) holds
H in {{},A1,(bool {{},1})}

let H be object ; :: thesis: ( H in the topology of ((ADTS (bool {{},1})) modified_with_respect_to A) implies H in {{},A1,(bool {{},1})} )
assume H in the topology of ((ADTS (bool {{},1})) modified_with_respect_to A) ; :: thesis: H in {{},A1,(bool {{},1})}
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: ( ( P = {} & Q = {} & H = {} ) or ( P = bool {{},1} & Q = {} & H = bool {{},1} ) or ( P = {} & Q = bool {{},1} & H = A ) or ( P = bool {{},1} & Q = bool {{},1} & H = bool {{},1} ) )

per cases ( ( P = {} & Q = {} ) or ( P = bool {{},1} & Q = {} ) or ( P = {} & Q = bool {{},1} ) or ( P = bool {{},1} & Q = bool {{},1} ) ) by A6, A7, TARSKI:def 2;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

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

end;

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

now :: thesis: for H being object st H in the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) holds
H in {{},A2,(A2 `),(bool {{},1})}

let H be object ; :: thesis: ( H in the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) implies H in {{},A2,(A2 `),(bool {{},1})} )
assume H in the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) ; :: thesis: H in {{},A2,(A2 `),(bool {{},1})}
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: ( ( P = {} & Q = {} & H = {} ) or ( P = A1 & Q = {} & H = A1 ) or ( P = bool {{},1} & Q = {} & H = bool {{},1} ) or ( P = {} & Q = A1 & H = {} ) or ( P = A1 & Q = A1 & H = A1 ) or ( P = bool {{},1} & Q = A1 & H = bool {{},1} ) or ( P = {} & Q = bool {{},1} & H = A2 ` ) or ( P = A1 & Q = bool {{},1} & H = bool {{},1} ) or ( P = bool {{},1} & Q = bool {{},1} & H = bool {{},1} ) )

per cases ( ( P = {} & Q = {} ) or ( P = A1 & Q = {} ) or ( P = bool {{},1} & Q = {} ) or ( P = {} & Q = A1 ) or ( P = A1 & Q = A1 ) or ( P = bool {{},1} & Q = A1 ) or ( P = {} & Q = bool {{},1} ) or ( P = A1 & Q = bool {{},1} ) or ( P = bool {{},1} & Q = bool {{},1} ) ) by A8, A10, A11, ENUMSET1:def 1;

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

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

end;

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

hence H = A1 by A9; :: thesis: verum

end;

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

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

end;

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

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

end;

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

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: verum

end;

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

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: verum

end;

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

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

end;

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

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: verum

end;

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

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

end;

end;

end;

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

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: for H being object st H in {{},A2,(A2 `),(bool {{},1})} holds
H in the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `))

let H be object ; :: thesis: ( H in {{},A2,(A2 `),(bool {{},1})} implies H in the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) )
assume H in {{},A2,(A2 `),(bool {{},1})} ; :: thesis: H in the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `))
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: verum

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: for G being Subset of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) st G is open holds
G is closed

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

A22: now :: thesis: ( G = A2 implies G is closed )

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: G is closed
hence G is closed by A23; :: thesis: verum

end;

A24: now :: thesis: ( G = A2 ` implies G is closed )

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: G is closed
hence G is closed by A25; :: thesis: verum

end;

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

end;

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

A27: now :: thesis: ex B being non empty Subset of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) st B is boundary

A28: now :: thesis: not Int B = A2 `

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: contradiction
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: verum

end;

take B = B; :: thesis: B is boundary

A31: now :: thesis: not Int B = A2

assume Int B = A2 ; :: thesis: contradiction
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: verum

end;

A33: now :: thesis: not Int B = bool {{},1}

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

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: verum

end;

take ((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `) ; :: thesis: ( ((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 )

now :: thesis: ex A2 being Subset of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) st
( A2 is open & A2 <> {} & A2 <> the carrier of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) )

take A2 = A2; :: thesis: ( A2 is open & A2 <> {} & A2 <> the carrier of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) )

now :: thesis: not A2 = bool {{},1}

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

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: verum

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: verum