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 consider P being Subset of T such that
A3: P = A0 and
A4: ex C being Subset of T st
( P = Int C & C in F ) ;
consider C being Subset of T such that
A5: P = Int C and
A6: C in F by A4;
thus Int (meet F) c= A by A3, A5, A6, SETFAM_1:4, TOPS_1:48; :: thesis: verum

end;

now

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

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

then ( meet F = {} T & meet (Int F) = {} T & Int ({} T) = {} T ) by Th19, SETFAM_1:2;
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:6; :: thesis: verum

end;

end;

end;

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