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 object st X in (Int F) \ (Int G) holds
X in Int (F \ G)

proof

let X be object ; :: 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 reconsider X0 = X as Subset of T ;
X in Int F by A1, XBOOLE_0:def 5;
then consider W being Subset of T such that
A2: X0 = Int W and
A3: W in F by Def1;
not X in Int G by A1, XBOOLE_0:def 5;
then not W in G by A2, Def1;
then W in F \ G by A3, XBOOLE_0:def 5;
hence X in Int (F \ G) by A2, Def1; :: thesis: verum

end;

hence (Int F) \ (Int G) c= Int (F \ G) ; :: thesis: verum