consider A being non empty set , m being BinOp of A, r being Function of n -tuples_on A,A;
take ReperAlgebraStr(# A,m,r #) ; :: thesis: not ReperAlgebraStr(# A,m,r #) is empty
thus not ReperAlgebraStr(# A,m,r #) is empty ; :: thesis: verum