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

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

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

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

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

end;

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

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

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

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

proof

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

end;

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

end;

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

end;

end;

end;

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