let X be set ; :: thesis: for F being Subset-Family of X st F c= Fin X holds

meet F in Fin X

let F be Subset-Family of X; :: thesis: ( F c= Fin X implies meet F in Fin X )

assume A1: F c= Fin X ; :: thesis: meet F in Fin X

meet F in Fin X

let F be Subset-Family of X; :: thesis: ( F c= Fin X implies meet F in Fin X )

assume A1: F c= Fin X ; :: thesis: meet F in Fin X