let T be non empty TopSpace; :: thesis:
let F be Subset-Family of T; :: thesis:

now :: thesis:

per cases ;

suppose F = {} ; :: thesis:

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

end;

suppose F <> {} ; :: thesis:

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

now :: thesis:

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

proof

let A be set ; :: thesis:
assume A3: A in Cl (Int (Cl F)) ; :: thesis:
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;
A6: B c= Cl B by PRE_TOPC:18;
x in B by A2, A5, SETFAM_1:def 1;
hence x in A by A4, A6; :: thesis:

end;

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

end;

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

end;

end;

end;

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