let T be TopSpace; :: thesis: for F, G being Subset-Family of T st F c= G holds
Fr F c= Fr G
let F, G be Subset-Family of T; :: thesis: ( F c= G implies Fr F c= Fr G )
assume A1: F c= G ; :: thesis: Fr F c= Fr G
Fr F c= Fr G

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Fr F or x in Fr G )
assume A2: x in Fr F ; :: thesis: x in Fr G
then reconsider A = x as Subset of T ;
ex B being Subset of T st
( A = Fr B & B in F ) by A2, Def1;
hence x in Fr G by A1, Def1; :: thesis: verum

end;

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