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

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

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

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

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: verum

end;

suppose F <> {} ; :: thesis: meet (Int (Cl 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 (Int (Cl F)) holds
x in meet (Cl (Int (Cl F)))

let x be object ; :: thesis: ( x in meet (Int (Cl F)) implies x in meet (Cl (Int (Cl F))) )
assume A2: x in meet (Int (Cl 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;
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: verum

end;

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

end;

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

end;

end;

end;

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