let A be Element of LTLB_WFF ; :: thesis: ( A = TFALSUM or ex n being Element of NAT st

( A = prop n or ex p, q being Element of LTLB_WFF st

( A = p => q or ex p, q being Element of LTLB_WFF st A = p 'U' q ) ) )

( A = VERUM or A is simple or A is conjunctive or A is conditional ) by HILBERT2:9;

hence ( A = TFALSUM or ex n being Element of NAT st

( A = prop n or ex p, q being Element of LTLB_WFF st

( A = p => q or ex p, q being Element of LTLB_WFF st A = p 'U' q ) ) ) by HILBERT2:def 6, HILBERT2:def 7, HILBERT2:def 8; :: thesis: verum

( A = prop n or ex p, q being Element of LTLB_WFF st

( A = p => q or ex p, q being Element of LTLB_WFF st A = p 'U' q ) ) )

( A = VERUM or A is simple or A is conjunctive or A is conditional ) by HILBERT2:9;

hence ( A = TFALSUM or ex n being Element of NAT st

( A = prop n or ex p, q being Element of LTLB_WFF st

( A = p => q or ex p, q being Element of LTLB_WFF st A = p 'U' q ) ) ) by HILBERT2:def 6, HILBERT2:def 7, HILBERT2:def 8; :: thesis: verum