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