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

Fr (union F) c= union (Fr F)

let F be Subset-Family of T; :: thesis: ( F is locally_finite implies Fr (union F) c= union (Fr F) )

assume F is locally_finite ; :: thesis: Fr (union F) c= union (Fr F)

then A1: Cl (union F) = union (clf F) by PCOMPS_1:20;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Fr (union F) or x in union (Fr F) )

assume x in Fr (union F) ; :: thesis: x in union (Fr F)

then A2: x in (Cl (union F)) /\ (Cl ((union F) `)) by TOPS_1:def 2;

then A3: x in Cl ((union F) `) by XBOOLE_0:def 4;

x in Cl (union F) by A2, XBOOLE_0:def 4;

then consider A being set such that

A4: x in A and

A5: A in clf F by A1, TARSKI:def 4;

consider B being Subset of T such that

A6: A = Cl B and

A7: B in F by A5, PCOMPS_1:def 2;

B c= union F by A7, ZFMISC_1:74;

then (union F) ` c= B ` by SUBSET_1:12;

then Cl ((union F) `) c= Cl (B `) by PRE_TOPC:19;

then x in (Cl B) /\ (Cl (B `)) by A4, A6, A3, XBOOLE_0:def 4;

then A8: x in Fr B by TOPS_1:def 2;

Fr B in Fr F by A7, TOPGEN_1:def 1;

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

Fr (union F) c= union (Fr F)

let F be Subset-Family of T; :: thesis: ( F is locally_finite implies Fr (union F) c= union (Fr F) )

assume F is locally_finite ; :: thesis: Fr (union F) c= union (Fr F)

then A1: Cl (union F) = union (clf F) by PCOMPS_1:20;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Fr (union F) or x in union (Fr F) )

assume x in Fr (union F) ; :: thesis: x in union (Fr F)

then A2: x in (Cl (union F)) /\ (Cl ((union F) `)) by TOPS_1:def 2;

then A3: x in Cl ((union F) `) by XBOOLE_0:def 4;

x in Cl (union F) by A2, XBOOLE_0:def 4;

then consider A being set such that

A4: x in A and

A5: A in clf F by A1, TARSKI:def 4;

consider B being Subset of T such that

A6: A = Cl B and

A7: B in F by A5, PCOMPS_1:def 2;

B c= union F by A7, ZFMISC_1:74;

then (union F) ` c= B ` by SUBSET_1:12;

then Cl ((union F) `) c= Cl (B `) by PRE_TOPC:19;

then x in (Cl B) /\ (Cl (B `)) by A4, A6, A3, XBOOLE_0:def 4;

then A8: x in Fr B by TOPS_1:def 2;

Fr B in Fr F by A7, TOPGEN_1:def 1;

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