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 } ;
set O = { U where U is Subset of X : not x0 in U } \/ { (F `) where F is Subset of X : F is finite } ;
set T = DiscrWithInfin (X,x0);
A1: the carrier of (DiscrWithInfin (X,x0)) = X by Def5;
A2: 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;
({} X) ` = X ;
then X in { (F `) where F is Subset of X : F is finite } ;
hence the carrier of (DiscrWithInfin (X,x0)) in the topology of (DiscrWithInfin (X,x0)) by A1, A2, XBOOLE_0:def 3; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b1 being Element of K32(K32( the carrier of (DiscrWithInfin (X,x0)))) holds
( not b1 c= the topology of (DiscrWithInfin (X,x0)) or union b1 in the topology of (DiscrWithInfin (X,x0)) ) ) & ( for b1, b2 being Element of K32( the carrier of (DiscrWithInfin (X,x0))) holds
( not b1 in the topology of (DiscrWithInfin (X,x0)) or not b2 in the topology of (DiscrWithInfin (X,x0)) or b1 /\ b2 in the topology of (DiscrWithInfin (X,x0)) ) ) )
hereby :: thesis: for b1, b2 being Element of K32( the carrier of (DiscrWithInfin (X,x0))) holds
( not b1 in the topology of (DiscrWithInfin (X,x0)) or not b2 in the topology of (DiscrWithInfin (X,x0)) or b1 /\ b2 in the topology of (DiscrWithInfin (X,x0)) )
let a be Subset-Family of (DiscrWithInfin (X,x0)); :: thesis: ( a c= the topology of (DiscrWithInfin (X,x0)) implies union b1 in the topology of (DiscrWithInfin (X,x0)) )
assume A3: a c= the topology of (DiscrWithInfin (X,x0)) ; :: thesis: union b1 in the topology of (DiscrWithInfin (X,x0))
per cases ( not a c= { U where U is Subset of X : not x0 in U } or a c= { U where U is Subset of X : not x0 in U } ) ;
suppose not a c= { U where U is Subset of X : not x0 in U } ; :: thesis: union b1 in the topology of (DiscrWithInfin (X,x0))
then consider b being object such that
A4: b in a and
A5: not b in { U where U is Subset of X : not x0 in U } ;
reconsider bb = b as set by TARSKI:1;
b in { (F `) where F is Subset of X : F is finite } by A2, A3, A4, A5, XBOOLE_0:def 3;
then A6: ex F being Subset of X st
( b = F ` & F is finite ) ;
A7: ((union a) `) ` = union a ;
bb c= union a by A4, ZFMISC_1:74;
then (union a) ` is finite by A1, A6, FINSET_1:1, SUBSET_1:17;
then union a in { (F `) where F is Subset of X : F is finite } by A1, A7;
hence union a in the topology of (DiscrWithInfin (X,x0)) by A2, XBOOLE_0:def 3; :: thesis: verum
end;
suppose A8: a c= { U where U is Subset of X : not x0 in U } ; :: thesis: union b1 in the topology of (DiscrWithInfin (X,x0))
now :: thesis: not x0 in union a
assume x0 in union a ; :: thesis: contradiction
then consider b being set such that
A9: x0 in b and
A10: b in a by TARSKI:def 4;
b in { U where U is Subset of X : not x0 in U } by A8, A10;
then ex U being Subset of X st
( b = U & not x0 in U ) ;
hence contradiction by A9; :: thesis: verum
end;
then union a in { U where U is Subset of X : not x0 in U } by A1;
hence union a in the topology of (DiscrWithInfin (X,x0)) by A2, XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
let a, b be Subset of (DiscrWithInfin (X,x0)); :: thesis: ( not a in the topology of (DiscrWithInfin (X,x0)) or not b in the topology of (DiscrWithInfin (X,x0)) or a /\ b in the topology of (DiscrWithInfin (X,x0)) )
assume that
A11: a in the topology of (DiscrWithInfin (X,x0)) and
A12: b in the topology of (DiscrWithInfin (X,x0)) ; :: thesis: a /\ b in the topology of (DiscrWithInfin (X,x0))
per cases ( ( a in { (F `) where F is Subset of X : F is finite } & b in { (F `) where F is Subset of X : F is finite } ) or a in { U where U is Subset of X : not x0 in U } or b in { U where U is Subset of X : not x0 in U } ) by A2, A11, A12, XBOOLE_0:def 3;
suppose A13: ( a in { (F `) where F is Subset of X : F is finite } & b in { (F `) where F is Subset of X : F is finite } ) ; :: thesis: a /\ b in the topology of (DiscrWithInfin (X,x0))
then consider F2 being Subset of X such that
A14: b = F2 ` and
A15: F2 is finite ;
consider F1 being Subset of X such that
A16: a = F1 ` and
A17: F1 is finite by A13;
a /\ b = (F1 \/ F2) ` by A16, A14, XBOOLE_1:53;
then a /\ b in { (F `) where F is Subset of X : F is finite } by A17, A15;
hence a /\ b in the topology of (DiscrWithInfin (X,x0)) by A2, XBOOLE_0:def 3; :: thesis: verum
end;
suppose ( a in { U where U is Subset of X : not x0 in U } or b in { U where U is Subset of X : not x0 in U } ) ; :: thesis: a /\ b in the topology of (DiscrWithInfin (X,x0))
then ( ex U being Subset of X st
( a = U & not x0 in U ) or ex U being Subset of X st
( b = U & not x0 in U ) ) ;
then not x0 in a /\ b by XBOOLE_0:def 4;
then a /\ b in { U where U is Subset of X : not x0 in U } by A1;
hence a /\ b in the topology of (DiscrWithInfin (X,x0)) by A2, XBOOLE_0:def 3; :: thesis: verum
end;
end;