let F, X be set ; :: thesis: ( X in F & X is ext-natural-membered implies meet F is ext-natural-membered )
assume A1: ( X in F & X is ext-natural-membered ) ; :: thesis: meet F is ext-natural-membered
let x be object ; :: according to COUNTERS:def 3 :: thesis: ( x in meet F implies x is ext-natural )
assume x in meet F ; :: thesis: x is ext-natural
then x in X by A1, SETFAM_1:def 1;
hence x is ext-natural by A1; :: thesis: verum