let T be TopSpace; :: thesis: for F, G being Subset-Family of T holds (Int F) \ (Int G) c= Int (F \ G)
let F, G be Subset-Family of T; :: thesis: (Int F) \ (Int G) c= Int (F \ G)
for X being set st X in (Int F) \ (Int G) holds
X in Int (F \ G)

proof

let X be set ; :: thesis: ( X in (Int F) \ (Int G) implies X in Int (F \ G) )
assume A1: X in (Int F) \ (Int G) ; :: thesis: X in Int (F \ G)
then A2: ( X in Int F & not X in Int G ) by XBOOLE_0:def 5;
reconsider X0 = X as Subset of T by A1;
consider W being Subset of T such that
A3: X0 = Int W and
A4: W in F by A2, Def1;
not W in G by A2, A3, Def1;
then W in F \ G by A4, XBOOLE_0:def 5;
hence X in Int (F \ G) by A3, Def1; :: thesis: verum

end;

hence (Int F) \ (Int G) c= Int (F \ G) by TARSKI:def 3; :: thesis: verum