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

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