thus ( the charact of UAStr(# the carrier of A,the charact of A #) <> {} & the charact of UAStr(# the carrier of A,the charact of A #) is non-empty ) ; :: according to UNIALG_1:def 9 :: thesis: verum