ex_inf_of {} ,L by YELLOW_0:43;
then "/\" (({} X),L) in fininfs X ;
hence not fininfs X is empty ; :: thesis: verum