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