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