let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is discrete holds
Cl () = union (clf F)

let F be Subset-Family of T; :: thesis: ( F is discrete implies Cl () = union (clf F) )
assume A1: F is discrete ; :: thesis: Cl () = union (clf F)
A2: Cl () c= union (clf F)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Cl () or x in union (clf F) )
assume A3: x in Cl () ; :: thesis: x in union (clf F)
then consider O being open Subset of T such that
A4: x in O and
A5: for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds
A = B by A1;
not O misses union F by ;
then consider f being object such that
A6: f in O and
A7: f in union F by XBOOLE_0:3;
consider AF being set such that
A8: f in AF and
A9: AF in F by ;
reconsider AF = AF as Subset of T by A9;
A10: O meets AF by ;
for D being Subset of T st D is open & x in D holds
not D misses AF
proof
assume ex D being Subset of T st
( D is open & x in D & D misses AF ) ; :: thesis: contradiction
then consider D being Subset of T such that
A11: D is open and
A12: x in D and
A13: D misses AF ;
x in D /\ O by ;
then D /\ O meets union F by ;
then consider y being object such that
A14: y in D /\ O and
A15: y in union F by XBOOLE_0:3;
consider BF being set such that
A16: y in BF and
A17: BF in F by ;
y in D by ;
then y in D /\ BF by ;
then A18: D meets BF by XBOOLE_0:def 7;
y in O by ;
then y in O /\ BF by ;
then O meets BF by XBOOLE_0:def 7;
hence contradiction by A5, A9, A10, A13, A17, A18; :: thesis: verum
end;
then A19: x in Cl AF by ;
Cl AF in clf F by ;
hence x in union (clf F) by ; :: thesis: verum
end;
union (clf F) c= Cl ()
proof
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in union (clf F) or f in Cl () )
assume f in union (clf F) ; :: thesis: f in Cl ()
then consider Af being set such that
A20: f in Af and
A21: Af in clf F by TARSKI:def 4;
reconsider Af = Af as Subset of T by A21;
ex A being Subset of T st
( Cl A = Af & A in F ) by ;
then Af c= Cl () by Lm4;
hence f in Cl () by A20; :: thesis: verum
end;
hence Cl () = union (clf F) by ; :: thesis: verum