let T be non empty TopSpace; :: thesis: for F being Subset-Family of T holds meet (Int (Cl (Int F))) c= meet (Int (Cl F))
let F be Subset-Family of T; :: thesis: meet (Int (Cl (Int F))) c= meet (Int (Cl F))

now :: thesis: meet (Int (Cl (Int F))) c= meet (Int (Cl F))

per cases ( F = {} or F <> {} ) ;

suppose F = {} ; :: thesis: meet (Int (Cl (Int F))) c= meet (Int (Cl F))

hence meet (Int (Cl (Int F))) c= meet (Int (Cl F)) by Th18; :: thesis: verum

end;

suppose F <> {} ; :: thesis: meet (Int (Cl (Int F))) c= meet (Int (Cl F))

then Cl F <> {} by Th9;
then A1: Int (Cl F) <> {} by Th18;

now :: thesis: for x being object st x in meet (Int (Cl (Int F))) holds
x in meet (Int (Cl F))

let x be object ; :: thesis: ( x in meet (Int (Cl (Int F))) implies x in meet (Int (Cl F)) )
assume A2: x in meet (Int (Cl (Int F))) ; :: thesis: x in meet (Int (Cl F))
for A being set st A in Int (Cl F) holds
x in A

proof

let A be set ; :: thesis: ( A in Int (Cl F) implies x in A )
assume A3: A in Int (Cl F) ; :: thesis: x in A
then reconsider A = A as Subset of T ;
consider E being Subset of T such that
A4: A = Int E and
A5: E in Cl F by A3, Def1;
consider B being Subset of T such that
A6: E = Cl B and
A7: B in F by A5, PCOMPS_1:def 2;
Int B in Int F by A7, Def1;
then Cl (Int B) in Cl (Int F) by PCOMPS_1:def 2;
then Int (Cl (Int B)) in Int (Cl (Int F)) by Def1;
then A8: x in Int (Cl (Int B)) by A2, SETFAM_1:def 1;
Int (Cl (Int B)) c= Int (Cl B) by Th1;
hence x in A by A4, A6, A8; :: thesis: verum

end;

hence x in meet (Int (Cl F)) by A1, SETFAM_1:def 1; :: thesis: verum

end;

hence meet (Int (Cl (Int F))) c= meet (Int (Cl F)) ; :: thesis: verum

end;

end;

end;

hence meet (Int (Cl (Int F))) c= meet (Int (Cl F)) ; :: thesis: verum