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 )
reconsider F0 = Int F, G0 = Int G as set ;
assume A1: F c= G ; :: thesis: Int F c= Int G

now :: thesis: for X being object st X in F0 holds
X in G0

let X be object ; :: 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 ;
ex V being Subset of T st
( X0 = Int V & V in F ) by A2, Def1;
hence X in G0 by A1, Def1; :: thesis: verum

end;

hence Int F c= Int G ; :: thesis: verum