take the empty RelStr ; :: thesis: the empty RelStr is empty
thus the empty RelStr is empty ; :: thesis: verum