reconsider F = bool the carrier of T as Subset-Family of T ;
reconsider F = F as Subset-Family of T ;
take F ; :: thesis: for A being Subset of T st p in Int A holds
ex P being Subset of T st
( P in F & p in Int P & P c= A )
let A be Subset of T; :: thesis: ( p in Int A implies ex P being Subset of T st
( P in F & p in Int P & P c= A ) )
assume A1: p in Int A ; :: thesis: ex P being Subset of T st
( P in F & p in Int P & P c= A )
take Int A ; :: thesis: ( Int A in F & p in Int (Int A) & Int A c= A )
thus ( Int A in F & p in Int (Int A) & Int A c= A ) by A1, TOPS_1:16; :: thesis: verum