let T be TopSpace; :: thesis: for F being Subset-Family of T holds Int (meet F) c= meet (Int F)
let F be Subset-Family of T; :: thesis: Int (meet F) c= meet (Int F)
A1: for A being set st A in Int F holds
Int (meet F) c= A

proof

let A be set ; :: thesis: ( A in Int F implies Int (meet F) c= A )
assume A2: A in Int F ; :: thesis: Int (meet F) c= A
then reconsider A0 = A as Subset of T ;
A0 in { B where B is Subset of T : ex C being Subset of T st
( B = Int C & C in F ) } by A2, Th16;
then ex P being Subset of T st
( P = A0 & ex C being Subset of T st
( P = Int C & C in F ) ) ;
hence Int (meet F) c= A by SETFAM_1:3, TOPS_1:19; :: thesis: verum

end;

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

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

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

then meet F = {} T by Th18, SETFAM_1:1;
hence Int (meet F) c= meet (Int F) ; :: thesis: verum

end;

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

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

end;

end;

end;

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