for F, X being set st X in F & X is ext-real-membered holds
meet F is ext-real-membered by Th20, SETFAM_1:3;