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:23;
let x be set ; :: 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 x in Cl (union F) by XBOOLE_0:def 4;
then consider A being set such that
A3: ( x in A & A in clf F ) by A1, TARSKI:def 4;
consider B being Subset of T such that
A4: ( A = Cl B & B in F ) by A3, PCOMPS_1:def 3;
A5: x in Cl ((union F) ` ) by A2, XBOOLE_0:def 4;
B c= union F by A4, ZFMISC_1:92;
then (union F) ` c= B ` by SUBSET_1:31;
then Cl ((union F) ` ) c= Cl (B ` ) by PRE_TOPC:49;
then A6: x in (Cl B) /\ (Cl (B ` )) by A3, A4, A5, XBOOLE_0:def 4;
A7: x in Fr B by A6, TOPS_1:def 2;
Fr B in Fr F by A4, TOPGEN_1:def 1;
hence x in union (Fr F) by A7, TARSKI:def 4; :: thesis: verum