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

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

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

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

end;

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

then A2: Cl F <> {} by Th9;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet (Cl (Int (Cl F))) or x in meet (Cl F) )
assume A3: x in meet (Cl (Int (Cl F))) ; :: thesis: x in meet (Cl F)
for A being set st A in Cl F holds
x in A

proof

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

end;

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

end;

end;