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