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:37;
A2: {} c= {{} ,1} by XBOOLE_1:2;
then reconsider A = {{} } as Subset of (ADTS (bool {{} ,1})) by 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;
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:104;
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:104;
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:104;
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 8;
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
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;
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
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 8;
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
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 ( P = {} & Q = bool {{} ,1} ) ; :: thesis: H = A2 `
hence H = A2 ` by A3, A4, A9, 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;
A17: A2 is open by Th1, TMAP_1:105;
A18: A2 is closed by Th3;
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, A4, A18, A17, 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 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
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: 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 ` )) ) by A4, TMAP_1:104;
hence G is closed ; :: thesis: verum
end;
A22: now
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 by PRE_TOPC:def 5;
assume G = A2 ; :: thesis: G is closed
hence G is closed by A23, TOPS_1:29; :: thesis: verum
end;
A24: now
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 by PRE_TOPC:def 5;
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, PRE_TOPC:def 5;
hence G is closed by A21, A22, A24, ENUMSET1:def 2; :: thesis: verum
end;
A26: {} in bool {{} ,1} by A2;
A27: now
A28: now
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:44;
assume Int B = A2 ` ; :: thesis: contradiction
then I in Int B by A29, SUBSET_1:50;
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
assume Int B = A2 ; :: thesis: contradiction
then A32: {} in Int B by TARSKI:def 1;
Int B c= B by TOPS_1:44;
hence contradiction by A32, TARSKI:def 2; :: thesis: verum
end;
A33: now
assume Int B = bool {{} ,1} ; :: thesis: contradiction
then bool {{} ,1} c= B by TOPS_1:44;
hence contradiction by A26, TARSKI:def 2; :: thesis: verum
end;
Int B in {{} ,A2,(A2 ` ),(bool {{} ,1})} by A19, PRE_TOPC:def 5;
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:84; :: 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
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, Th1, TMAP_1:104, TMAP_1:105; :: 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, Def6, TDLAT_3:20, TDLAT_3:23; :: thesis: verum