ex p, q being Element of LTLB_WFF st p 'U' q = A by A1, HILBERT2:def 6;
hence ex b₁, p being Element of LTLB_WFF st p 'U' b₁ = A ; :: thesis: verum