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

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

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

then Int F = {} by Th18;
then Cl (Int F) = {} by Th9;
hence meet (Int (Cl (Int F))) c= meet (Cl (Int F)) by Th18; :: thesis: verum

end;

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

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

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

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

proof

let A be set ; :: thesis: ( A in Cl (Int F) implies x in A )
assume A3: A in Cl (Int F) ; :: thesis: x in A
then reconsider A = A as Subset of T ;
consider E being Subset of T such that
A4: A = Cl E and
A5: E in Int F by A3, PCOMPS_1:def 2;
consider B being Subset of T such that
A6: E = Int B and
A7: B in F by A5, Def1;
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= Cl (Int B) by Th1;
hence x in A by A4, A6, A8; :: thesis: verum

end;

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

end;

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

end;

end;