( finsups X = { ("\/" Y,L) where Y is finite Subset of X : ex_sup_of Y,L } & ex_sup_of {} ,L ) by YELLOW_0:42;
then "\/" ({} X),L in finsups X ;
hence not finsups X is empty ; :: thesis: verum