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