set C = bool {{} ,1};
set Y = ADTS (bool {{} ,1});
A1: {} c= {{} ,1} by XBOOLE_1:2;
then A2: {} in bool {{} ,1} ;
reconsider A = {{} } as Subset of (ADTS (bool {{} ,1})) by A1, ZFMISC_1:37;
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:104;
reconsider A1 = A as Subset of ((ADTS (bool {{} ,1})) modified_with_respect_to A) by TMAP_1:104;
A4: A1 is open by TMAP_1:105;
now
let H be set ; :: 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:104;
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})) & Q in the topology of (ADTS (bool {{} ,1})) ) ;
now
per cases ( ( P = {} & Q = {} ) or ( P = bool {{} ,1} & Q = {} ) or ( P = {} & Q = bool {{} ,1} ) or ( P = bool {{} ,1} & Q = bool {{} ,1} ) ) by A6, 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;
end;
end;
hence H in {{} ,A1,(bool {{} ,1})} by ENUMSET1:def 1; :: thesis: verum
end;
then A7: the topology of ((ADTS (bool {{} ,1})) modified_with_respect_to A) c= {{} ,A1,(bool {{} ,1})} by TARSKI:def 3;
set Y2 = ((ADTS (bool {{} ,1})) modified_with_respect_to A) modified_with_respect_to (A1 ` );
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 )
A8: 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:104;
reconsider A2 = A1 as Subset of (((ADTS (bool {{} ,1})) modified_with_respect_to A) modified_with_respect_to (A1 ` )) by TMAP_1:104;
set A3 = A2 ` ;
A9: ( A2 is closed & A2 is open ) by A4, Th1, Th3;
now
let H be set ; :: 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:104;
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
A11: H = P \/ (Q /\ (A1 ` )) and
A12: ( 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) ) ;
now
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 A7, A12, ENUMSET1:def 1;
case ( P = {} & Q = {} ) ; :: thesis: H = {}
hence H = {} by A11; :: thesis: verum
end;
case ( P = A1 & Q = {} ) ; :: thesis: H = A1
hence H = A1 by A11; :: thesis: verum
end;
case ( P = bool {{} ,1} & Q = {} ) ; :: thesis: H = bool {{} ,1}
hence H = bool {{} ,1} by A11; :: thesis: verum
end;
case ( P = {} & Q = bool {{} ,1} ) ; :: thesis: H = A2 `
hence H = A2 ` by A3, A8, A11, XBOOLE_1:28; :: 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;
now
let H be set ; :: 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, A8, A9, PRE_TOPC:5, PRE_TOPC:def 1, PRE_TOPC:def 5; :: 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 A17: 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;
( {} in {{} ,1} & 1 in {{} ,1} ) by TARSKI:def 2;
then reconsider B0 = {{} }, B1 = {1} as Subset of {{} ,1} by ZFMISC_1:37;
reconsider B = {B0,B1} as non empty Subset of (((ADTS (bool {{} ,1})) modified_with_respect_to A) modified_with_respect_to (A1 ` )) by A8, TMAP_1:104;
A18: now
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
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, A8, Th1, TMAP_1:104; :: thesis: verum
end;
A19: now
take B = B; :: thesis: B is boundary
Int B in {{} ,A2,(A2 ` ),(bool {{} ,1})} by A17, PRE_TOPC:def 5;
then A20: ( Int B = {} or Int B = A2 or Int B = A2 ` or Int B = bool {{} ,1} ) by ENUMSET1:def 2;
A21: now
assume Int B = bool {{} ,1} ; :: thesis: contradiction
then bool {{} ,1} c= B by TOPS_1:44;
hence contradiction by A2, TARSKI:def 2; :: thesis: verum
end;
A22: now
assume Int B = A2 ; :: thesis: contradiction
then ( {} in Int B & Int B c= B ) by TARSKI:def 1, TOPS_1:44;
hence contradiction by TARSKI:def 2; :: thesis: verum
end;
now
assume A23: Int B = A2 ` ; :: thesis: contradiction
reconsider I = {{} ,1} as Point of (((ADTS (bool {{} ,1})) modified_with_respect_to A) modified_with_respect_to (A1 ` )) by A3, A8, ZFMISC_1:def 1;
not I in A2 by TARSKI:def 1;
then ( I in Int B & Int B c= B ) by A23, SUBSET_1:50, TOPS_1:44;
then ( I = B0 or I = B1 ) by TARSKI:def 2;
then ( 1 in B0 or {} in B1 ) by TARSKI:def 2;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
hence B is boundary by A20, A21, A22, TOPS_1:84; :: thesis: verum
end;
now
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 )
assume G is open ; :: thesis: G is closed
then A24: G in {{} ,A2,(A2 ` ),(bool {{} ,1})} by A17, PRE_TOPC:def 5;
A25: now
assume ( G = {} or G = bool {{} ,1} ) ; :: thesis: G is closed
then ( ( G = {} (((ADTS (bool {{} ,1})) modified_with_respect_to A) modified_with_respect_to (A1 ` )) or G = [#] (((ADTS (bool {{} ,1})) modified_with_respect_to A) modified_with_respect_to (A1 ` )) ) & {} (((ADTS (bool {{} ,1})) modified_with_respect_to A) modified_with_respect_to (A1 ` )) is closed & [#] (((ADTS (bool {{} ,1})) modified_with_respect_to A) modified_with_respect_to (A1 ` )) is closed ) by A8, TMAP_1:104;
hence G is closed ; :: thesis: verum
end;
A26: now
assume A27: G = A2 ; :: thesis: G is closed
A2 ` in the topology of (((ADTS (bool {{} ,1})) modified_with_respect_to A) modified_with_respect_to (A1 ` )) by A17, ENUMSET1:def 2;
then A2 ` is open by PRE_TOPC:def 5;
hence G is closed by A27, TOPS_1:29; :: thesis: verum
end;
now
assume A28: G = A2 ` ; :: thesis: G is closed
A2 in the topology of (((ADTS (bool {{} ,1})) modified_with_respect_to A) modified_with_respect_to (A1 ` )) by A17, ENUMSET1:def 2;
then (A2 ` ) ` is open by PRE_TOPC:def 5;
hence G is closed by A28; :: thesis: verum
end;
hence G is closed by A24, A25, A26, ENUMSET1:def 2; :: 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 A18, A19, Def6, TDLAT_3:20, TDLAT_3:23; :: thesis: verum