let T be TopSpace; :: thesis: for F being Subset-Family of T holds Int F = Int (Int F)
let F be Subset-Family of T; :: thesis: Int F = Int (Int F)
A1: Int F = { A where A is Subset of T : ex B being Subset of T st
( A = Int B & B in F ) } by Th16;
A2: Int (Int F) = { D where D is Subset of T : ex B being Subset of T st
( D = Int B & B in Int F ) } by Th16;
for X being set holds
( X in Int F iff X in Int (Int F) )

proof

let X be set ; :: thesis: ( X in Int F iff X in Int (Int F) )

A3: now

assume A4: X in Int F ; :: thesis: X in Int (Int F)
then reconsider C = X as Subset of T ;
consider B being Subset of T such that
A5: C = Int B and
A6: B in F by A4, Def1;
( C = Int (Int B) & Int B in Int F ) by A5, A6, Def1;
hence X in Int (Int F) by A2; :: thesis: verum

end;

now

assume A7: X in Int (Int F) ; :: thesis: X in Int F
then reconsider C = X as Subset of T ;
ex Q being Subset of T st
( Q = C & ex B being Subset of T st
( Q = Int B & B in Int F ) ) by A2, A7;
then consider B being Subset of T such that
A8: C = Int B and
A9: B in Int F ;
ex Q being Subset of T st
( Q = B & ex R being Subset of T st
( Q = Int R & R in F ) ) by A1, A9;
then consider R being Subset of T such that
A10: B = Int R and
A11: R in F ;
thus X in Int F by A8, A10, A11, Def1; :: thesis: verum

end;

hence ( X in Int F iff X in Int (Int F) ) by A3; :: thesis: verum

end;

hence Int F = Int (Int F) by TARSKI:2; :: thesis: verum