let T be TopSpace; :: thesis: for A being Subset of T
for F being Subset-Family of T st F = {A} holds
Int F = {(Int A)}
let A be Subset of T; :: thesis: for F being Subset-Family of T st F = {A} holds
Int F = {(Int A)}
let F be Subset-Family of T; :: thesis: ( F = {A} implies Int F = {(Int A)} )
reconsider C = Int F as set ;
assume A1: F = {A} ; :: thesis: Int F = {(Int A)}
for B being object holds
( B in C iff B = Int A )

proof

let B be object ; :: thesis: ( B in C iff B = Int A )

A2: now :: thesis: ( B = Int A implies B in C )

assume A3: B = Int A ; :: thesis: B in C
ex M being Subset of T st
( B = Int M & M in F )

proof

take A ; :: thesis: ( B = Int A & A in F )
thus ( B = Int A & A in F ) by A1, A3, TARSKI:def 1; :: thesis: verum

end;

hence B in C by Def1; :: thesis: verum

end;

now :: thesis: ( B in C implies B = Int A )

assume A4: B in C ; :: thesis: B = Int A
then reconsider B0 = B as Subset of T ;
ex M being Subset of T st
( B0 = Int M & M in F ) by A4, Def1;
hence B = Int A by A1, TARSKI:def 1; :: thesis: verum

end;

hence ( B in C iff B = Int A ) by A2; :: thesis: verum

end;

hence Int F = {(Int A)} by TARSKI:def 1; :: thesis: verum