take TrivLattRelStr ; :: thesis: not TrivLattRelStr is empty
thus not TrivLattRelStr is empty ; :: thesis: verum