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