ex_sup_of {} ,L by YELLOW_0:42;
then "\/" ({} X),L in finsups X ;
hence not finsups X is empty ; :: thesis: verum