Finseq-EQclass the Element of S * in distribution_family S by Def6;
hence not distribution_family S is empty ; :: thesis: verum