let A be uncountable set ; :: thesis:
set TS = 1TopSp [:A,A:];
set F = { ([:{a},A:] \/ [:A,{a}:]) where a is Element of A : a in A } ;
{ ([:{a},A:] \/ [:A,{a}:]) where a is Element of A : a in A } c= bool [:A,A:]

let f be object ; :: according to TARSKI:def 3 :: thesis:
assume f in { ([:{a},A:] \/ [:A,{a}:]) where a is Element of A : a in A } ; :: thesis:
then consider a being Element of A such that
A1: f = [:{a},A:] \/ [:A,{a}:] and
a in A ;
( [:{a},A:] c= [:A,A:] & [:A,{a}:] c= [:A,A:] ) by ZFMISC_1:96;
then [:{a},A:] \/ [:A,{a}:] c= [:A,A:] by XBOOLE_1:8;
hence f in bool [:A,A:] by A1; :: thesis:

end;

then reconsider F = { ([:{a},A:] \/ [:A,{a}:]) where a is Element of A : a in A } as Subset-Family of (1TopSp [:A,A:]) ;
take F ; :: thesis:
for z being Point of (1TopSp [:A,A:]) ex Z being Subset of (1TopSp [:A,A:]) st
( z in Z & Z is open & { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } is finite )

proof

let z be Point of (1TopSp [:A,A:]); :: thesis:
set Z = {z};
reconsider Z = {z} as Subset of (1TopSp [:A,A:]) ;
consider x, y being object such that
x in A and
y in A and
A2: z = [x,y] by ZFMISC_1:def 2;
set yAAy = {([:{y},A:] \/ [:A,{y}:])};
set xAAx = {([:{x},A:] \/ [:A,{x}:])};
set UZ = { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } ;
A3: { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } c= {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])}

proof

let U be object ; :: according to TARSKI:def 3 :: thesis:
assume U in { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } ; :: thesis:
then consider O being Subset of (1TopSp [:A,A:]) such that
A4: U = O and
A5: O in F and
A6: O meets Z ;
consider u being object such that
A7: u in O and
A8: u in Z by A6, XBOOLE_0:3;
consider a being Element of A such that
A9: O = [:{a},A:] \/ [:A,{a}:] and
a in A by A5;

now :: thesis:

per cases by A9, A7, XBOOLE_0:def 3;

suppose u in [:{a},A:] ; :: thesis:

then [x,y] in [:{a},A:] by A2, A8, TARSKI:def 1;
then x in {a} by ZFMISC_1:87;
then x = a by TARSKI:def 1;
then O in {([:{x},A:] \/ [:A,{x}:])} by A9, TARSKI:def 1;
hence O in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])} by XBOOLE_0:def 3; :: thesis:

end;

suppose u in [:A,{a}:] ; :: thesis:

then [x,y] in [:A,{a}:] by A2, A8, TARSKI:def 1;
then y in {a} by ZFMISC_1:87;
then y = a by TARSKI:def 1;
then O in {([:{y},A:] \/ [:A,{y}:])} by A9, TARSKI:def 1;
hence O in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])} by XBOOLE_0:def 3; :: thesis:

end;

hence U in {([:{x},A:] \/ [:A,{x}:])} \/ {([:{y},A:] \/ [:A,{y}:])} by A4; :: thesis:

end;

( z in Z & Z is open ) by PRE_TOPC:def 2, ZFMISC_1:31;
hence ex Z being Subset of (1TopSp [:A,A:]) st
( z in Z & Z is open & { O where O is Subset of (1TopSp [:A,A:]) : ( O in F & O meets Z ) } is finite ) by A3; :: thesis:

end;

hence F is locally_finite ; :: thesis:
not F is sigma_discrete

proof

consider a being object such that
A10: a in A by XBOOLE_0:def 1;
reconsider a = a as Element of A by A10;
set aAAa = [:{a},A:] \/ [:A,{a}:];
A11: card A c= card F

proof

deffunc H₁( object ) -> set = [:{$1},A:] \/ [:A,{$1}:];
consider d being Function such that
A12: ( dom d = A & ( for x being object st x in A holds
d . x = H₁(x) ) ) from FUNCT_1:sch 3();
for a1, a2 being object st a1 in dom d & a2 in dom d & d . a1 = d . a2 holds
a1 = a2

proof

let a1, a2 be object ; :: thesis:
assume that
A13: a1 in dom d and
A14: a2 in dom d and
A15: d . a1 = d . a2 ; :: thesis:
a1 in {a1} by ZFMISC_1:31;
then A16: [a1,a1] in [:{a1},A:] by A12, A13, ZFMISC_1:87;
( H₁(a1) = d . a1 & H₁(a2) = d . a2 ) by A12, A13, A14;
then [a1,a1] in [:{a2},A:] \/ [:A,{a2}:] by A15, A16, XBOOLE_0:def 3;
then ( [a1,a1] in [:{a2},A:] or [a1,a1] in [:A,{a2}:] ) by XBOOLE_0:def 3;
then A17: a1 in {a2} by ZFMISC_1:87;
assume a1 <> a2 ; :: thesis:
hence contradiction by A17, TARSKI:def 1; :: thesis:

end;

then A18: d is one-to-one by FUNCT_1:def 4;
rng d c= F

proof

let AA be object ; :: according to TARSKI:def 3 :: thesis:
assume AA in rng d ; :: thesis:
then consider a being object such that
A19: a in dom d and
A20: AA = d . a by FUNCT_1:def 3;
reconsider a = a as Element of A by A12, A19;
AA = [:{a},A:] \/ [:A,{a}:] by A12, A20;
hence AA in F ; :: thesis:

end;

hence card A c= card F by A12, A18, CARD_1:10; :: thesis:

end;

assume F is sigma_discrete ; :: thesis:
then consider f being sigma_discrete FamilySequence of (1TopSp [:A,A:]) such that
A21: F = Union f ;
defpred S₁[ object , object ] means ( ( $2 in f . $1 & not f . $1 is empty ) or ( $2 = [:{a},A:] \/ [:A,{a}:] & f . $1 is empty ) );
A22: for k being object st k in NAT holds
ex f being object st
( f in F & S₁[k,f] )

proof

let k be object ; :: thesis:
assume k in NAT ; :: thesis:
then reconsider k = k as Element of NAT ;

now :: thesis:

per cases ;

suppose A23: f . k is empty ; :: thesis:

[:{a},A:] \/ [:A,{a}:] in F ;
hence ex A being set st
( A in F & S₁[k,A] ) by A23; :: thesis:

end;

suppose not f . k is empty ; :: thesis:

then consider A being object such that
A24: A in f . k by XBOOLE_0:def 1;
A in F by A21, A24, PROB_1:12;
hence ex A being set st
( A in F & S₁[k,A] ) by A24; :: thesis:

end;

hence ex f being object st
( f in F & S₁[k,f] ) ; :: thesis:

end;

consider Df being sequence of F such that
A25: for k being object st k in NAT holds
S₁[k,Df . k] from FUNCT_2:sch 1(A22);
A26: for n being Element of NAT
for AD, BD being Element of F st S₁[n,AD] & S₁[n,BD] holds
AD = BD

proof

let n be Element of NAT ; :: thesis:
let AD, BD be Element of F; :: thesis:
assume that
A27: S₁[n,AD] and
A28: S₁[n,BD] ; :: thesis:

now :: thesis:

A29: f . n is discrete by Def2;
BD in F by A21, A28, PROB_1:12;
then consider b being Element of A such that
A30: BD = [:{b},A:] \/ [:A,{b}:] and
b in A ;
AD in F by A21, A27, PROB_1:12;
then consider a being Element of A such that
A31: AD = [:{a},A:] \/ [:A,{a}:] and
a in A ;
b in {b} by TARSKI:def 1;
then [a,b] in [:A,{b}:] by ZFMISC_1:87;
then A32: [a,b] in BD by A30, XBOOLE_0:def 3;
a in {a} by TARSKI:def 1;
then [a,b] in [:{a},A:] by ZFMISC_1:87;
then [a,b] in AD by A31, XBOOLE_0:def 3;
then AD meets BD by A32, XBOOLE_0:3;
hence AD = BD by A27, A28, A29, Th6; :: thesis:

end;

hence AD = BD ; :: thesis:

end;

A33: F c= Df .: NAT

proof

let cAAc be object ; :: according to TARSKI:def 3 :: thesis:
assume A34: cAAc in F ; :: thesis:
then consider k being Nat such that
A35: cAAc in f . k by A21, PROB_1:12;
A36: k in NAT by ORDINAL1:def 12;
S₁[k,Df . k] by A25, A36;
then A37: cAAc = Df . k by A26, A34, A35, A36;
dom Df = NAT by A34, FUNCT_2:def 1;
hence cAAc in Df .: NAT by A37, FUNCT_1:def 6, A36; :: thesis:

end;

A38: not card A c= omega by CARD_3:def 14;
then card NAT in card A by CARD_1:4, CARD_1:47;
then card NAT c= card F by A11, CARD_1:3;
then card NAT c< card F by A11, A38, CARD_1:47, XBOOLE_0:def 8;
then A39: card (Df .: NAT) c< card F by CARD_1:67, XBOOLE_1:59;
then card (Df .: NAT) c= card F by XBOOLE_0:def 8;
then card (Df .: NAT) in card F by A39, CARD_1:3;
then F \ (Df .: NAT) <> {} by CARD_1:68;
hence contradiction by A33, XBOOLE_1:37; :: thesis:

end;

hence not F is sigma_discrete ; :: thesis: