let T be non empty TopSpace; :: thesis: for F being Subset-Family of T holds union (Int (Cl F)) c= union (Cl (Int (Cl F)))
let F be Subset-Family of T; :: thesis: union (Int (Cl F)) c= union (Cl (Int (Cl F)))
now :: thesis: for x being object st x in union (Int (Cl F)) holds
x in union (Cl (Int (Cl F)))
let x be object ; :: thesis: ( x in union (Int (Cl F)) implies x in union (Cl (Int (Cl F))) )
assume x in union (Int (Cl F)) ; :: thesis: x in union (Cl (Int (Cl F)))
then consider A being set such that
A1: x in A and
A2: A in Int (Cl F) by TARSKI:def 4;
reconsider A = A as Subset of T by A2;
consider B being Subset of T such that
A3: A = Int B and
A4: B in Cl F by A2, Def1;
consider D being Subset of T such that
A5: B = Cl D and
A6: D in F by A4, PCOMPS_1:def 2;
ex P being set st
( x in P & P in Cl (Int (Cl F)) )
proof
take Cl (Int (Cl D)) ; :: thesis: ( x in Cl (Int (Cl D)) & Cl (Int (Cl D)) in Cl (Int (Cl F)) )
Cl D in Cl F by A6, PCOMPS_1:def 2;
then A7: Int (Cl D) in Int (Cl F) by Def1;
A c= Cl (Int (Cl D)) by A3, A5, Th2;
hence ( x in Cl (Int (Cl D)) & Cl (Int (Cl D)) in Cl (Int (Cl F)) ) by A1, A7, PCOMPS_1:def 2; :: thesis: verum
end;
hence x in union (Cl (Int (Cl F))) by TARSKI:def 4; :: thesis: verum
end;
hence union (Int (Cl F)) c= union (Cl (Int (Cl F))) ; :: thesis: verum