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

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

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

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

end;

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

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

proof

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

end;

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

end;

end;