let T be TopSpace; :: thesis: for F, G being Subset-Family of T holds Fr (F \/ G) = (Fr F) \/ (Fr G)
let F, G be Subset-Family of T; :: thesis: Fr (F \/ G) = (Fr F) \/ (Fr G)
thus Fr (F \/ G) c= (Fr F) \/ (Fr G) :: according to XBOOLE_0:def 10 :: thesis: (Fr F) \/ (Fr G) c= Fr (F \/ G)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Fr (F \/ G) or x in (Fr F) \/ (Fr G) )
assume A1: x in Fr (F \/ G) ; :: thesis: x in (Fr F) \/ (Fr G)
then reconsider A = x as Subset of T ;
consider B being Subset of T such that
A2: A = Fr B and
A3: B in F \/ G by A1, Def1;

per cases ( B in F or B in G ) by A3, XBOOLE_0:def 3;

suppose B in F ; :: thesis: x in (Fr F) \/ (Fr G)

then A in Fr F by A2, Def1;
hence x in (Fr F) \/ (Fr G) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose B in G ; :: thesis: x in (Fr F) \/ (Fr G)

then A in Fr G by A2, Def1;
hence x in (Fr F) \/ (Fr G) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

( Fr F c= Fr (F \/ G) & Fr G c= Fr (F \/ G) ) by Th6, XBOOLE_1:7;
hence (Fr F) \/ (Fr G) c= Fr (F \/ G) by XBOOLE_1:8; :: thesis: verum