thus the charact of TRSStr(# X,O,r #) <> {} ; :: according to UNIALG_1:def 3 :: thesis: the charact of TRSStr(# X,O,r #) is non-empty
thus the charact of TRSStr(# X,O,r #) is non-empty ; :: thesis: verum