let T be TopSpace; :: thesis: for F being Subset-Family of T holds
( F = {} iff Int F = {} )
let F be Subset-Family of T; :: thesis: ( F = {} iff Int F = {} )
thus ( F = {} implies Int F = {} ) :: thesis: ( Int F = {} implies F = {} )
proof
set A = the Element of Int F;
assume A1: F = {} ; :: thesis: Int F = {}
assume A2: not Int F = {} ; :: thesis: contradiction
then reconsider A = the Element of Int F as Subset of T by TARSKI:def 3;
ex V being Subset of T st
( A = Int V & V in F ) by A2, Def1;
hence contradiction by A1; :: thesis: verum
end;
thus ( Int F = {} implies F = {} ) :: thesis: verum
proof
set B = the Element of F;
assume A3: Int F = {} ; :: thesis: F = {}
assume A4: not F = {} ; :: thesis: contradiction
then reconsider B = the Element of F as Subset of T by TARSKI:def 3;
reconsider A = Int B as set ;
ex A being set st A in Int F
proof
take A ; :: thesis: A in Int F
thus A in Int F by A4, Def1; :: thesis: verum
end;
hence contradiction by A3; :: thesis: verum
end;