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