set A = the Element of F;
reconsider A = the Element of F as non empty ext-real-membered set by SETFAM_1:def 8;
inf A = inf A ;
hence not INF F is empty by Def4; :: thesis: verum