set x = the Element of X;
reconsider y = the Element of X as Element of L ;
reconsider Z = {y} as finite Subset of X by ZFMISC_1:31;
ex_sup_of Z,L by YELLOW_0:38;
then "\/" (Z,L) in finsups X ;
hence not finsups X is empty ; :: thesis: verum