s in Finseq-EQclass s ;
hence not Finseq-EQclass s is empty ; :: thesis: verum