let T be TopSpace; :: thesis: for F, G being Subset-Family of T st F c= G holds
Int F c= Int G
let F, G be Subset-Family of T; :: thesis: ( F c= G implies Int F c= Int G )
assume A1: F c= G ; :: thesis: Int F c= Int G
reconsider F0 = Int F, G0 = Int G as set ;

now

let X be set ; :: thesis: ( X in F0 implies X in G0 )
assume A2: X in F0 ; :: thesis: X in G0
then reconsider X0 = X as Subset of T ;
consider V being Subset of T such that
A3: X0 = Int V and
A4: V in F by A2, Def1;
thus X in G0 by A1, A3, A4, Def1; :: thesis: verum

end;

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