consider A being Element of F;
reconsider A = A as non empty ext-real-membered set by SETFAM_1:def 9;
inf A = inf A ;
hence not INF F is empty by Def20; :: thesis: verum