let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st ( for A being Subset of T st A in F holds
Int (Cl A) c= A ) holds
( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) )
let F be Subset-Family of T; :: thesis: ( ( for A being Subset of T st A in F holds
Int (Cl A) c= A ) implies ( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) ) )
A1: Int (Int (meet F)) c= Int (Cl (Int (meet F))) by PRE_TOPC:18, TOPS_1:19;
assume A2: for A being Subset of T st A in F holds
Int (Cl A) c= A ; :: thesis: ( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) )
thus Int (Cl (meet F)) c= meet F :: thesis: Int (Cl (Int (meet F))) = Int (meet F)

proof

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

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

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

Cl ({} T) = {} T by PRE_TOPC:22;
hence Int (Cl (meet F)) c= meet F by A3, SETFAM_1:1; :: thesis: verum

end;

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

now :: thesis: for A0 being set st A0 in F holds
Int (Cl (meet F)) c= A0

let A0 be set ; :: thesis: ( A0 in F implies Int (Cl (meet F)) c= A0 )
assume A5: A0 in F ; :: thesis: Int (Cl (meet F)) c= A0
then reconsider A = A0 as Subset of T ;
Cl (meet F) c= Cl A by A5, PRE_TOPC:19, SETFAM_1:3;
then A6: Int (Cl (meet F)) c= Int (Cl A) by TOPS_1:19;
Int (Cl A) c= A by A2, A5;
hence Int (Cl (meet F)) c= A0 by A6; :: thesis: verum

end;

hence Int (Cl (meet F)) c= meet F by A4, SETFAM_1:5; :: thesis: verum

end;

end;

end;

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

end;

then A7: Int (Int (Cl (meet F))) c= Int (meet F) by TOPS_1:19;
Cl (Int (meet F)) c= Cl (meet F) by PRE_TOPC:19, TOPS_1:16;
then Int (Cl (Int (meet F))) c= Int (Cl (meet F)) by TOPS_1:19;
then Int (Cl (Int (meet F))) c= Int (meet F) by A7;
hence Int (Cl (Int (meet F))) = Int (meet F) by A1, XBOOLE_0:def 10; :: thesis: verum