set f = U -concatenation ;
e /\ (U -concatenation) is U -concatenation -unambiguous ;
hence for b₁ being set st b₁ = e /\ U holds
b₁ is U -prefix ; :: thesis: verum