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

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