take {} /\ U ; :: thesis: {} /\ U is U -prefix
thus {} /\ U is U -prefix ; :: thesis: verum