take PrefSpace {} ; :: thesis: PrefSpace {} is total
thus PrefSpace {} is total ; :: thesis: verum