let T be non empty TopSpace; :: thesis: for F being Subset-Family of T holds
( ( for B being Subset of T st B in F holds
Int (meet F) c= B ) & ( F = {} or for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= Int (meet F) ) )
let F be Subset-Family of T; :: thesis: ( ( for B being Subset of T st B in F holds
Int (meet F) c= B ) & ( F = {} or for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= Int (meet F) ) )
thus for B being Subset of T st B in F holds
Int (meet F) c= B :: thesis: ( F = {} or for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= Int (meet F) )
proof
let B be Subset of T; :: thesis: ( B in F implies Int (meet F) c= B )
assume B in F ; :: thesis: Int (meet F) c= B
then A1: meet F c= B by SETFAM_1:3;
Int (meet F) c= meet F by TOPS_1:16;
hence Int (meet F) c= B by A1; :: thesis: verum
end;
thus ( F = {} or for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= Int (meet F) ) :: thesis: verum
proof
assume A2: F <> {} ; :: thesis: for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
A c= B ) holds
A c= Int (meet F)
let A be Subset of T; :: thesis: ( A is open_condensed & ( for B being Subset of T st B in F holds
A c= B ) implies A c= Int (meet F) )
assume A3: A is open_condensed ; :: thesis: ( ex B being Subset of T st
( B in F & not A c= B ) or A c= Int (meet F) )
assume for B being Subset of T st B in F holds
A c= B ; :: thesis: A c= Int (meet F)
then for P being set st P in F holds
A c= P ;
then A4: A c= meet F by A2, SETFAM_1:5;
A is open by A3, TOPS_1:67;
then Int A = A by TOPS_1:23;
hence A c= Int (meet F) by A4, TOPS_1:19; :: thesis: verum
end;