take UMF C ; :: thesis: UMF C is normalized
thus UMF C is normalized ; :: thesis: verum