let X, x0 be set ; :: thesis: for A being Subset of (DiscrWithInfin (X,x0)) holds
( A is open iff ( not x0 in A or A ` is finite ) )
set T = DiscrWithInfin (X,x0);
set O1 = { U where U is Subset of X : not x0 in U } ;
set O2 = { (F `) where F is Subset of X : F is finite } ;
let A be Subset of (DiscrWithInfin (X,x0)); :: thesis: ( A is open iff ( not x0 in A or A ` is finite ) )
A1: the topology of (DiscrWithInfin (X,x0)) = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } by Def5;
A2: the carrier of (DiscrWithInfin (X,x0)) = X by Def5;
thus ( not A is open or not x0 in A or A ` is finite ) :: thesis: ( ( not x0 in A or A ` is finite ) implies A is open )
proof
assume A in the topology of (DiscrWithInfin (X,x0)) ; :: according to PRE_TOPC:def 2 :: thesis: ( not x0 in A or A ` is finite )
then ( A in { U where U is Subset of X : not x0 in U } or A in { (F `) where F is Subset of X : F is finite } ) by A1, XBOOLE_0:def 3;
then ( ex U being Subset of X st
( A = U & not x0 in U ) or ex F being Subset of X st
( A = F ` & F is finite ) ) ;
hence ( not x0 in A or A ` is finite ) by A2; :: thesis: verum
end;
assume ( not x0 in A or A ` is finite ) ; :: thesis: A is open
then ( A in { U where U is Subset of X : not x0 in U } or (A `) ` in { (F `) where F is Subset of X : F is finite } ) by A2;
hence A in the topology of (DiscrWithInfin (X,x0)) by A1, XBOOLE_0:def 3; :: according to PRE_TOPC:def 2 :: thesis: verum