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 3 :: thesis: verum