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 (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;
A2: Int F = { A where A is Subset of T : ex B being Subset of T st
( A = Int B & B in 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 (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 A1, A4;
then consider B being Subset of T such that
A5: C = Int B and
A6: 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 A2, A6;
hence X in Int F by A5, Def1; :: thesis: verum

end;

now

assume A7: 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
A8: C = Int B and
A9: B in F by A7, Def1;
A10: C = Int (Int B) by A8;
Int B in Int F by A9, Def1;
hence X in Int (Int F) by A1, A10; :: 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