let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is discrete holds

Cl (union F) = union (clf F)

let F be Subset-Family of T; :: thesis: ( F is discrete implies Cl (union F) = union (clf F) )

assume A1: F is discrete ; :: thesis: Cl (union F) = union (clf F)

A2: Cl (union F) c= union (clf F)

Cl (union F) = union (clf F)

let F be Subset-Family of T; :: thesis: ( F is discrete implies Cl (union F) = union (clf F) )

assume A1: F is discrete ; :: thesis: Cl (union F) = union (clf F)

A2: Cl (union F) c= union (clf F)

proof

union (clf F) c= Cl (union F)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Cl (union F) or x in union (clf F) )

assume A3: x in Cl (union F) ; :: 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 A3, A4, PRE_TOPC:def 7;

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 A7, TARSKI:def 4;

reconsider AF = AF as Subset of T by A9;

A10: O meets AF by A6, A8, XBOOLE_0:3;

for D being Subset of T st D is open & x in D holds

not D misses AF

Cl AF in clf F by A9, PCOMPS_1:def 2;

hence x in union (clf F) by A19, TARSKI:def 4; :: thesis: verum

end;assume A3: x in Cl (union F) ; :: 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 A3, A4, PRE_TOPC:def 7;

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 A7, TARSKI:def 4;

reconsider AF = AF as Subset of T by A9;

A10: O meets AF by A6, A8, XBOOLE_0:3;

for D being Subset of T st D is open & x in D holds

not D misses AF

proof

then A19:
x in Cl AF
by A3, PRE_TOPC:def 7;
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 A4, A12, XBOOLE_0:def 4;

then D /\ O meets union F by A3, A11, PRE_TOPC:def 7;

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 A15, TARSKI:def 4;

y in D by A14, XBOOLE_0:def 4;

then y in D /\ BF by A16, XBOOLE_0:def 4;

then A18: D meets BF by XBOOLE_0:def 7;

y in O by A14, XBOOLE_0:def 4;

then y in O /\ BF by A16, XBOOLE_0:def 4;

then O meets BF by XBOOLE_0:def 7;

hence contradiction by A5, A9, A10, A13, A17, A18; :: thesis: verum

end;( 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 A4, A12, XBOOLE_0:def 4;

then D /\ O meets union F by A3, A11, PRE_TOPC:def 7;

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 A15, TARSKI:def 4;

y in D by A14, XBOOLE_0:def 4;

then y in D /\ BF by A16, XBOOLE_0:def 4;

then A18: D meets BF by XBOOLE_0:def 7;

y in O by A14, XBOOLE_0:def 4;

then y in O /\ BF by A16, XBOOLE_0:def 4;

then O meets BF by XBOOLE_0:def 7;

hence contradiction by A5, A9, A10, A13, A17, A18; :: thesis: verum

Cl AF in clf F by A9, PCOMPS_1:def 2;

hence x in union (clf F) by A19, TARSKI:def 4; :: thesis: verum

proof

hence
Cl (union F) = union (clf F)
by A2, XBOOLE_0:def 10; :: thesis: verum
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in union (clf F) or f in Cl (union F) )

assume f in union (clf F) ; :: thesis: f in Cl (union F)

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 A21, PCOMPS_1:def 2;

then Af c= Cl (union F) by Lm4;

hence f in Cl (union F) by A20; :: thesis: verum

end;assume f in union (clf F) ; :: thesis: f in Cl (union F)

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 A21, PCOMPS_1:def 2;

then Af c= Cl (union F) by Lm4;

hence f in Cl (union F) by A20; :: thesis: verum