let C be Cardinal; :: thesis: for T being TopSpace st ( for A being Subset of T st A is discrete holds
card A c= C ) holds
for F being Subset-Family of T st F is open & not {} in F & ( for A, B being Subset of T st A in F & B in F & A <> B holds
A misses B ) holds
card F c= C
let T be TopSpace; :: thesis: ( ( for A being Subset of T st A is discrete holds
card A c= C ) implies for F being Subset-Family of T st F is open & not {} in F & ( for A, B being Subset of T st A in F & B in F & A <> B holds
A misses B ) holds
card F c= C )
assume A1: for A being Subset of T st A is discrete holds
card A c= C ; :: thesis: for F being Subset-Family of T st F is open & not {} in F & ( for A, B being Subset of T st A in F & B in F & A <> B holds
A misses B ) holds
card F c= C
let F be Subset-Family of T; :: thesis: ( F is open & not {} in F & ( for A, B being Subset of T st A in F & B in F & A <> B holds
A misses B ) implies card F c= C )
assume that
A2: F is open and
A3: not {} in F and
A4: for A, B being Subset of T st A in F & B in F & A <> B holds
A misses B ; :: thesis: card F c= C

per cases ( F is empty or not F is empty ) ;

suppose F is empty ; :: thesis: card F c= C

hence card F c= C ; :: thesis: verum

end;

suppose A5: not F is empty ; :: thesis: card F c= C

deffunc H₁( set ) -> Element of $1 = the Element of $1;
A6: for x being set st x in F holds
H₁(x) in [#] T

proof

let x be set ; :: thesis: ( x in F implies H₁(x) in [#] T )
assume A7: x in F ; :: thesis: H₁(x) in [#] T
then x <> {} by A3;
then H₁(x) in x ;
hence H₁(x) in [#] T by A7; :: thesis: verum

end;

consider p being Function of F,([#] T) such that
A8: for x being set st x in F holds
p . x = H₁(x) from FUNCT_2:sch 11(A6);
reconsider RNG = rng p as Subset of T ;
ex xx being object st xx in F by A5;
then A9: not T is empty by A3;
then A10: dom p = F by FUNCT_2:def 1;
for x being Point of T st x in RNG holds
ex G being Subset of T st
( G is open & RNG /\ G = {x} )

proof

let x be Point of T; :: thesis: ( x in RNG implies ex G being Subset of T st
( G is open & RNG /\ G = {x} ) )
assume A11: x in RNG ; :: thesis: ex G being Subset of T st
( G is open & RNG /\ G = {x} )
then consider G being object such that
A12: G in F and
A13: p . G = x by A10, FUNCT_1:def 3;
reconsider G = G as Subset of T by A12;
A14: RNG /\ G c= {x}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in RNG /\ G or y in {x} )
assume A15: y in RNG /\ G ; :: thesis: y in {x}
then A16: y in G by XBOOLE_0:def 4;
y in RNG by A15, XBOOLE_0:def 4;
then consider z being object such that
A17: z in F and
A18: p . z = y by A10, FUNCT_1:def 3;
reconsider z = z as set by TARSKI:1;
y = H₁(z) by A8, A17, A18;
then z meets G by A3, A16, A17, XBOOLE_0:3;
then x = y by A4, A12, A13, A17, A18;
hence y in {x} by TARSKI:def 1; :: thesis: verum

end;

take G ; :: thesis: ( G is open & RNG /\ G = {x} )
thus G is open by A2, A12; :: thesis: RNG /\ G = {x}
x = H₁(G) by A8, A12, A13;
then x in RNG /\ G by A3, A11, A12, XBOOLE_0:def 4;
hence RNG /\ G = {x} by A14, ZFMISC_1:33; :: thesis: verum

end;

then A19: card RNG c= C by A1, A9, TEX_2:31;
for x1, x2 being object st x1 in dom p & x2 in dom p & p . x1 = p . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom p & x2 in dom p & p . x1 = p . x2 implies x1 = x2 )
assume that
A20: x1 in dom p and
A21: x2 in dom p and
A22: p . x1 = p . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as set by TARSKI:1;
A23: ( p . x2 = H₁(x2) & x2 <> {} ) by A3, A8, A21;
( p . x1 = H₁(x1) & x1 <> {} ) by A3, A8, A20;
then x1 meets x2 by A22, A23, XBOOLE_0:3;
hence x1 = x2 by A4, A10, A20, A21; :: thesis: verum

end;

then p is one-to-one by FUNCT_1:def 4;
then card F c= card RNG by A10, CARD_1:10;
hence card F c= C by A19; :: thesis: verum

end;

end;