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; PRE_TOPC:def 1 ( ( 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 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));
( 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))
;
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 }
;
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;
verum end; end;
end;
let a, b be Subset of (DiscrWithInfin (X,x0)); ( 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))
; a /\ b in the topology of (DiscrWithInfin (X,x0))