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) ) )
assume A1: 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 A2: Int (Cl (meet F)) c= meet F :: thesis: Int (Cl (Int (meet F))) = Int (meet F)

proof

now

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

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

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

end;

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

now

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:49, SETFAM_1:4;
then ( Int (Cl (meet F)) c= Int (Cl A) & Int (Cl A) c= A ) by A1, A5, TOPS_1:48;
hence Int (Cl (meet F)) c= A0 by XBOOLE_1:1; :: thesis: verum

end;

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

end;

end;

end;

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

end;

thus Int (Cl (Int (meet F))) = Int (meet F) :: thesis: verum

proof

( Int (Cl (meet F)) c= meet F & Int (meet F) c= meet F ) by A2, TOPS_1:44;
then ( Int (Int (Cl (meet F))) c= Int (meet F) & Cl (Int (meet F)) c= Cl (meet F) ) by PRE_TOPC:49, TOPS_1:48;
then ( Int (Cl (meet F)) c= Int (meet F) & Int (Cl (Int (meet F))) c= Int (Cl (meet F)) ) by TOPS_1:48;
then A6: Int (Cl (Int (meet F))) c= Int (meet F) by XBOOLE_1:1;
Int (Int (meet F)) c= Int (Cl (Int (meet F))) by PRE_TOPC:48, TOPS_1:48;
hence Int (Cl (Int (meet F))) = Int (meet F) by A6, XBOOLE_0:def 10; :: thesis: verum

end;