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