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