let T be TopSpace; :: thesis: for F being Subset-Family of T holds meet (Int F) c= meet F
let F be Subset-Family of T; :: thesis: meet (Int F) c= meet F
A1: for A being set st A in F holds
meet (Int F) c= A
proof
let A be set ; :: thesis: ( A in F implies meet (Int F) c= A )
assume A2: A in F ; :: thesis: meet (Int F) c= A
then reconsider A0 = A as Subset of T ;
set C = Int A0;
Int A0 in { P where P is Subset of T : ex Q being Subset of T st
( P = Int Q & Q in F ) } by A2;
then Int A0 in Int F by Th16;
then A3: meet (Int F) c= Int A0 by SETFAM_1:3;
Int A0 c= A0 by TOPS_1:16;
hence meet (Int F) c= A by A3; :: thesis: verum
end;
now :: thesis: meet (Int F) c= meet F
per cases ( F = {} or F <> {} ) ;
end;
end;
hence meet (Int F) c= meet F ; :: thesis: verum