let T be TopSpace; :: thesis: for F being Subset-Family of T
for A being Subset of T st F = {A} holds
Fr F = {(Fr A)}
let F be Subset-Family of T; :: thesis: for A being Subset of T st F = {A} holds
Fr F = {(Fr A)}
let A be Subset of T; :: thesis: ( F = {A} implies Fr F = {(Fr A)} )
assume A1: F = {A} ; :: thesis: Fr F = {(Fr A)}
thus Fr F c= {(Fr A)} :: according to XBOOLE_0:def 10 :: thesis: {(Fr A)} c= Fr F
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Fr F or x in {(Fr A)} )
assume A2: x in Fr F ; :: thesis: x in {(Fr A)}
then reconsider B = x as Subset of T ;
consider C being Subset of T such that
A3: B = Fr C and
A4: C in F by A2, Def1;
C = A by A1, A4, TARSKI:def 1;
hence x in {(Fr A)} by A3, TARSKI:def 1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(Fr A)} or x in Fr F )
assume x in {(Fr A)} ; :: thesis: x in Fr F
then A5: x = Fr A by TARSKI:def 1;
A in F by A1, TARSKI:def 1;
hence x in Fr F by A5, Def1; :: thesis: verum